H-Termination proof of /home/matraf/haskell/eval_FullyBlown

MAYBE 17.712 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could not be shown:

↳ HASKELL

  ↳ LR

mainModule Main

((ceiling :: Float -> Int) :: Float -> Int)

module Main where

import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(_,r)→r

is transformed to

r0 (_,r) = r

The following Lambda expression

\(n,_)→n

is transformed to

n0 (n,_) = n

The following Lambda expression

\(_,r)→r

is transformed to

r1 (_,r) = r

The following Lambda expression

\(q,_)→q

is transformed to

q1 (q,_) = q

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

mainModule Main

((ceiling :: Float -> Int) :: Float -> Int)

module Main where

import qualified Prelude

If Reductions:
The following If expression

if r > 0 then n + 1 else n

is transformed to

ceiling0 True = n + 1

ceiling0 False = n

The following If expression

if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to

primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))

primDivNatS0 x y False = Zero

The following If expression

if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to

primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)

primModNatS0 x y False = Succ x

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

mainModule Main

((ceiling :: Float -> Int) :: Float -> Int)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern

frac@(Double vz wu)

is replaced by the following term

Double vz wu

The bind variable of the following binding Pattern

frac@(Float wx wy)

is replaced by the following term

Float wx wy

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

mainModule Main

((ceiling :: Float -> Int) :: Float -> Int)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

mainModule Main

((ceiling :: Float -> Int) :: Float -> Int)

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

ceiling0 (r > 0)

where

ceiling0 True = n + 1

ceiling0 False = n

n = n0 vu8

n0 (n,vw) = n

r = r0 vu8

r0 (vv,r) = r

vu8 = properFraction x

are unpacked to the following functions on top level

ceilingN0 xx (n,vw) = n

ceilingR0 xx (vv,r) = r

ceilingVu8 xx = properFraction xx

ceilingR xx = ceilingR0 xx (ceilingVu8 xx)

ceilingCeiling0 xx True = ceilingN xx + 1

ceilingCeiling0 xx False = ceilingN xx

ceilingN xx = ceilingN0 xx (ceilingVu8 xx)

The bindings of the following Let/Where expression

(fromIntegral q,r :% y)

where

q = q1 vu30

q1 (q,xu) = q

r = r1 vu30

r1 (xv,r) = r

vu30 = quotRem x y

are unpacked to the following functions on top level

properFractionQ1 xy xz (q,xu) = q

properFractionR1 xy xz (xv,r) = r

properFractionR xy xz = properFractionR1 xy xz (properFractionVu30 xy xz)

properFractionVu30 xy xz = quotRem xy xz

properFractionQ xy xz = properFractionQ1 xy xz (properFractionVu30 xy xz)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

mainModule Main

((ceiling :: Float -> Int) :: Float -> Int)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                          ↳ Narrow

mainModule Main

(ceiling :: Float -> Int)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="ceiling",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="ceiling yu3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="ceilingCeiling0 yu3 (ceilingR yu3 > fromInt (Pos Zero))",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="ceilingCeiling0 yu3 (compare (ceilingR yu3) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="ceilingCeiling0 yu3 (primCmpFloat (ceilingR yu3) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="ceilingCeiling0 yu3 (primCmpFloat (ceilingR0 yu3 (ceilingVu8 yu3)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="ceilingCeiling0 yu3 (primCmpFloat (ceilingR0 yu3 (properFraction yu3)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="ceilingCeiling0 yu3 (primCmpFloat (ceilingR0 yu3 (floatProperFractionFloat yu3)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6190[label="yu3/Float yu30 yu31",fontsize=10,color="white",style="solid",shape="box"];9 -> 6190[label="",style="solid", color="burlywood", weight=9];
6190 -> 10[label="",style="solid", color="burlywood", weight=3];
10[label="ceilingCeiling0 (Float yu30 yu31) (primCmpFloat (ceilingR0 (Float yu30 yu31) (floatProperFractionFloat (Float yu30 yu31))) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];10 -> 11[label="",style="solid", color="black", weight=3];
11[label="ceilingCeiling0 (Float yu30 yu31) (primCmpFloat (ceilingR0 (Float yu30 yu31) (fromInt (yu30 `quot` yu31),Float yu30 yu31 - fromInt (yu30 `quot` yu31))) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="ceilingCeiling0 (Float yu30 yu31) (primCmpFloat (Float yu30 yu31 - fromInt (yu30 `quot` yu31)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];12 -> 13[label="",style="solid", color="black", weight=3];
13[label="ceilingCeiling0 (Float yu30 yu31) (primCmpFloat (primMinusFloat (Float yu30 yu31) (fromInt (yu30 `quot` yu31))) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];13 -> 14[label="",style="solid", color="black", weight=3];
14[label="ceilingCeiling0 (Float yu30 yu31) (primCmpFloat (primMinusFloat (Float yu30 yu31) (primIntToFloat (yu30 `quot` yu31))) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];14 -> 15[label="",style="solid", color="black", weight=3];
15[label="ceilingCeiling0 (Float yu30 yu31) (primCmpFloat (primMinusFloat (Float yu30 yu31) (Float (yu30 `quot` yu31) (Pos (Succ Zero)))) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];15 -> 16[label="",style="solid", color="black", weight=3];
16[label="ceilingCeiling0 (Float yu30 yu31) (primCmpFloat (Float (yu30 - yu30 `quot` yu31) (yu31 * Pos (Succ Zero))) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];16 -> 17[label="",style="solid", color="black", weight=3];
17[label="ceilingCeiling0 (Float yu30 yu31) (primCmpFloat (Float (yu30 - yu30 `quot` yu31) (yu31 * Pos (Succ Zero))) (primIntToFloat (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];17 -> 18[label="",style="solid", color="black", weight=3];
18[label="ceilingCeiling0 (Float yu30 yu31) (primCmpFloat (Float (yu30 - yu30 `quot` yu31) (yu31 * Pos (Succ Zero))) (Float (Pos Zero) (Pos (Succ Zero))) == GT)",fontsize=16,color="black",shape="box"];18 -> 19[label="",style="solid", color="black", weight=3];
19[label="ceilingCeiling0 (Float yu30 yu31) (compare ((yu30 - yu30 `quot` yu31) * Pos Zero) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];19 -> 20[label="",style="solid", color="black", weight=3];
20[label="ceilingCeiling0 (Float yu30 yu31) (primCmpInt ((yu30 - yu30 `quot` yu31) * Pos Zero) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];20 -> 21[label="",style="solid", color="black", weight=3];
21[label="ceilingCeiling0 (Float yu30 yu31) (primCmpInt (primMulInt (yu30 - yu30 `quot` yu31) (Pos Zero)) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];21 -> 22[label="",style="solid", color="black", weight=3];
22[label="ceilingCeiling0 (Float yu30 yu31) (primCmpInt (primMulInt (primMinusInt yu30 (yu30 `quot` yu31)) (Pos Zero)) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6191[label="yu30/Pos yu300",fontsize=10,color="white",style="solid",shape="box"];22 -> 6191[label="",style="solid", color="burlywood", weight=9];
6191 -> 23[label="",style="solid", color="burlywood", weight=3];
6192[label="yu30/Neg yu300",fontsize=10,color="white",style="solid",shape="box"];22 -> 6192[label="",style="solid", color="burlywood", weight=9];
6192 -> 24[label="",style="solid", color="burlywood", weight=3];
23[label="ceilingCeiling0 (Float (Pos yu300) yu31) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (Pos yu300 `quot` yu31)) (Pos Zero)) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];23 -> 25[label="",style="solid", color="black", weight=3];
24[label="ceilingCeiling0 (Float (Neg yu300) yu31) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (Neg yu300 `quot` yu31)) (Pos Zero)) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];24 -> 26[label="",style="solid", color="black", weight=3];
25[label="ceilingCeiling0 (Float (Pos yu300) yu31) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) yu31)) (Pos Zero)) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6193[label="yu31/Pos yu310",fontsize=10,color="white",style="solid",shape="box"];25 -> 6193[label="",style="solid", color="burlywood", weight=9];
6193 -> 27[label="",style="solid", color="burlywood", weight=3];
6194[label="yu31/Neg yu310",fontsize=10,color="white",style="solid",shape="box"];25 -> 6194[label="",style="solid", color="burlywood", weight=9];
6194 -> 28[label="",style="solid", color="burlywood", weight=3];
26[label="ceilingCeiling0 (Float (Neg yu300) yu31) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) yu31)) (Pos Zero)) (yu31 * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6195[label="yu31/Pos yu310",fontsize=10,color="white",style="solid",shape="box"];26 -> 6195[label="",style="solid", color="burlywood", weight=9];
6195 -> 29[label="",style="solid", color="burlywood", weight=3];
6196[label="yu31/Neg yu310",fontsize=10,color="white",style="solid",shape="box"];26 -> 6196[label="",style="solid", color="burlywood", weight=9];
6196 -> 30[label="",style="solid", color="burlywood", weight=3];
27[label="ceilingCeiling0 (Float (Pos yu300) (Pos yu310)) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) (Pos yu310))) (Pos Zero)) (Pos yu310 * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6197[label="yu310/Succ yu3100",fontsize=10,color="white",style="solid",shape="box"];27 -> 6197[label="",style="solid", color="burlywood", weight=9];
6197 -> 31[label="",style="solid", color="burlywood", weight=3];
6198[label="yu310/Zero",fontsize=10,color="white",style="solid",shape="box"];27 -> 6198[label="",style="solid", color="burlywood", weight=9];
6198 -> 32[label="",style="solid", color="burlywood", weight=3];
28[label="ceilingCeiling0 (Float (Pos yu300) (Neg yu310)) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) (Neg yu310))) (Pos Zero)) (Neg yu310 * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6199[label="yu310/Succ yu3100",fontsize=10,color="white",style="solid",shape="box"];28 -> 6199[label="",style="solid", color="burlywood", weight=9];
6199 -> 33[label="",style="solid", color="burlywood", weight=3];
6200[label="yu310/Zero",fontsize=10,color="white",style="solid",shape="box"];28 -> 6200[label="",style="solid", color="burlywood", weight=9];
6200 -> 34[label="",style="solid", color="burlywood", weight=3];
29[label="ceilingCeiling0 (Float (Neg yu300) (Pos yu310)) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) (Pos yu310))) (Pos Zero)) (Pos yu310 * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6201[label="yu310/Succ yu3100",fontsize=10,color="white",style="solid",shape="box"];29 -> 6201[label="",style="solid", color="burlywood", weight=9];
6201 -> 35[label="",style="solid", color="burlywood", weight=3];
6202[label="yu310/Zero",fontsize=10,color="white",style="solid",shape="box"];29 -> 6202[label="",style="solid", color="burlywood", weight=9];
6202 -> 36[label="",style="solid", color="burlywood", weight=3];
30[label="ceilingCeiling0 (Float (Neg yu300) (Neg yu310)) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) (Neg yu310))) (Pos Zero)) (Neg yu310 * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6203[label="yu310/Succ yu3100",fontsize=10,color="white",style="solid",shape="box"];30 -> 6203[label="",style="solid", color="burlywood", weight=9];
6203 -> 37[label="",style="solid", color="burlywood", weight=3];
6204[label="yu310/Zero",fontsize=10,color="white",style="solid",shape="box"];30 -> 6204[label="",style="solid", color="burlywood", weight=9];
6204 -> 38[label="",style="solid", color="burlywood", weight=3];
31[label="ceilingCeiling0 (Float (Pos yu300) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) (Pos (Succ yu3100)))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];31 -> 39[label="",style="solid", color="black", weight=3];
32[label="ceilingCeiling0 (Float (Pos yu300) (Pos Zero)) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) (Pos Zero))) (Pos Zero)) (Pos Zero * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];32 -> 40[label="",style="solid", color="black", weight=3];
33[label="ceilingCeiling0 (Float (Pos yu300) (Neg (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) (Neg (Succ yu3100)))) (Pos Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];33 -> 41[label="",style="solid", color="black", weight=3];
34[label="ceilingCeiling0 (Float (Pos yu300) (Neg Zero)) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (primQuotInt (Pos yu300) (Neg Zero))) (Pos Zero)) (Neg Zero * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];34 -> 42[label="",style="solid", color="black", weight=3];
35[label="ceilingCeiling0 (Float (Neg yu300) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) (Pos (Succ yu3100)))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];35 -> 43[label="",style="solid", color="black", weight=3];
36[label="ceilingCeiling0 (Float (Neg yu300) (Pos Zero)) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) (Pos Zero))) (Pos Zero)) (Pos Zero * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];36 -> 44[label="",style="solid", color="black", weight=3];
37[label="ceilingCeiling0 (Float (Neg yu300) (Neg (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) (Neg (Succ yu3100)))) (Pos Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];37 -> 45[label="",style="solid", color="black", weight=3];
38[label="ceilingCeiling0 (Float (Neg yu300) (Neg Zero)) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (primQuotInt (Neg yu300) (Neg Zero))) (Pos Zero)) (Neg Zero * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];38 -> 46[label="",style="solid", color="black", weight=3];
39[label="ceilingCeiling0 (Float (Pos yu300) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (Pos (primDivNatS yu300 (Succ yu3100)))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];39 -> 47[label="",style="solid", color="black", weight=3];
40[label="ceilingCeiling0 (Float (Pos yu300) (Pos Zero)) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (error [])) (Pos Zero)) (Pos Zero * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];40 -> 48[label="",style="solid", color="black", weight=3];
41[label="ceilingCeiling0 (Float (Pos yu300) (Neg (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (Neg (primDivNatS yu300 (Succ yu3100)))) (Pos Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];41 -> 49[label="",style="solid", color="black", weight=3];
42[label="ceilingCeiling0 (Float (Pos yu300) (Neg Zero)) (primCmpInt (primMulInt (primMinusInt (Pos yu300) (error [])) (Pos Zero)) (Neg Zero * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];42 -> 50[label="",style="solid", color="black", weight=3];
43[label="ceilingCeiling0 (Float (Neg yu300) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (Neg (primDivNatS yu300 (Succ yu3100)))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];43 -> 51[label="",style="solid", color="black", weight=3];
44[label="ceilingCeiling0 (Float (Neg yu300) (Pos Zero)) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (error [])) (Pos Zero)) (Pos Zero * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];44 -> 52[label="",style="solid", color="black", weight=3];
45[label="ceilingCeiling0 (Float (Neg yu300) (Neg (Succ yu3100))) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (Pos (primDivNatS yu300 (Succ yu3100)))) (Pos Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];45 -> 53[label="",style="solid", color="black", weight=3];
46[label="ceilingCeiling0 (Float (Neg yu300) (Neg Zero)) (primCmpInt (primMulInt (primMinusInt (Neg yu300) (error [])) (Pos Zero)) (Neg Zero * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];46 -> 54[label="",style="solid", color="black", weight=3];
47[label="ceilingCeiling0 (Float (Pos yu300) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat yu300 (primDivNatS yu300 (Succ yu3100))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6205[label="yu300/Succ yu3000",fontsize=10,color="white",style="solid",shape="box"];47 -> 6205[label="",style="solid", color="burlywood", weight=9];
6205 -> 55[label="",style="solid", color="burlywood", weight=3];
6206[label="yu300/Zero",fontsize=10,color="white",style="solid",shape="box"];47 -> 6206[label="",style="solid", color="burlywood", weight=9];
6206 -> 56[label="",style="solid", color="burlywood", weight=3];
48[label="error []",fontsize=16,color="red",shape="box"];49[label="ceilingCeiling0 (Float (Pos yu300) (Neg (Succ yu3100))) (primCmpInt (primMulInt (Pos (primPlusNat yu300 (primDivNatS yu300 (Succ yu3100)))) (Pos Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];49 -> 57[label="",style="solid", color="black", weight=3];
50[label="error []",fontsize=16,color="red",shape="box"];51[label="ceilingCeiling0 (Float (Neg yu300) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (primDivNatS yu300 (Succ yu3100)) yu300) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6207[label="yu300/Succ yu3000",fontsize=10,color="white",style="solid",shape="box"];51 -> 6207[label="",style="solid", color="burlywood", weight=9];
6207 -> 58[label="",style="solid", color="burlywood", weight=3];
6208[label="yu300/Zero",fontsize=10,color="white",style="solid",shape="box"];51 -> 6208[label="",style="solid", color="burlywood", weight=9];
6208 -> 59[label="",style="solid", color="burlywood", weight=3];
52[label="error []",fontsize=16,color="red",shape="box"];53[label="ceilingCeiling0 (Float (Neg yu300) (Neg (Succ yu3100))) (primCmpInt (primMulInt (Neg (primPlusNat yu300 (primDivNatS yu300 (Succ yu3100)))) (Pos Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];53 -> 60[label="",style="solid", color="black", weight=3];
54[label="error []",fontsize=16,color="red",shape="box"];55[label="ceilingCeiling0 (Float (Pos (Succ yu3000)) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (Succ yu3000) (primDivNatS (Succ yu3000) (Succ yu3100))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];55 -> 61[label="",style="solid", color="black", weight=3];
56[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat Zero (primDivNatS Zero (Succ yu3100))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];56 -> 62[label="",style="solid", color="black", weight=3];
57[label="ceilingCeiling0 (Float (Pos yu300) (Neg (Succ yu3100))) (primCmpInt (Pos (primMulNat (primPlusNat yu300 (primDivNatS yu300 (Succ yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6209[label="yu300/Succ yu3000",fontsize=10,color="white",style="solid",shape="box"];57 -> 6209[label="",style="solid", color="burlywood", weight=9];
6209 -> 63[label="",style="solid", color="burlywood", weight=3];
6210[label="yu300/Zero",fontsize=10,color="white",style="solid",shape="box"];57 -> 6210[label="",style="solid", color="burlywood", weight=9];
6210 -> 64[label="",style="solid", color="burlywood", weight=3];
58[label="ceilingCeiling0 (Float (Neg (Succ yu3000)) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (primDivNatS (Succ yu3000) (Succ yu3100)) (Succ yu3000)) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];58 -> 65[label="",style="solid", color="black", weight=3];
59[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (primDivNatS Zero (Succ yu3100)) Zero) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];59 -> 66[label="",style="solid", color="black", weight=3];
60[label="ceilingCeiling0 (Float (Neg yu300) (Neg (Succ yu3100))) (primCmpInt (Neg (primMulNat (primPlusNat yu300 (primDivNatS yu300 (Succ yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6211[label="yu300/Succ yu3000",fontsize=10,color="white",style="solid",shape="box"];60 -> 6211[label="",style="solid", color="burlywood", weight=9];
6211 -> 67[label="",style="solid", color="burlywood", weight=3];
6212[label="yu300/Zero",fontsize=10,color="white",style="solid",shape="box"];60 -> 6212[label="",style="solid", color="burlywood", weight=9];
6212 -> 68[label="",style="solid", color="burlywood", weight=3];
61[label="ceilingCeiling0 (Float (Pos (Succ yu3000)) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (Succ yu3000) (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6213[label="yu3000/Succ yu30000",fontsize=10,color="white",style="solid",shape="box"];61 -> 6213[label="",style="solid", color="burlywood", weight=9];
6213 -> 69[label="",style="solid", color="burlywood", weight=3];
6214[label="yu3000/Zero",fontsize=10,color="white",style="solid",shape="box"];61 -> 6214[label="",style="solid", color="burlywood", weight=9];
6214 -> 70[label="",style="solid", color="burlywood", weight=3];
62[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat Zero Zero) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];62 -> 71[label="",style="solid", color="black", weight=3];
63[label="ceilingCeiling0 (Float (Pos (Succ yu3000)) (Neg (Succ yu3100))) (primCmpInt (Pos (primMulNat (primPlusNat (Succ yu3000) (primDivNatS (Succ yu3000) (Succ yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];63 -> 72[label="",style="solid", color="black", weight=3];
64[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos (primMulNat (primPlusNat Zero (primDivNatS Zero (Succ yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];64 -> 73[label="",style="solid", color="black", weight=3];
65 -> 2969[label="",style="dashed", color="red", weight=0];
65[label="ceilingCeiling0 (Float (Neg (Succ yu3000)) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100)) (Succ yu3000)) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="magenta"];65 -> 2970[label="",style="dashed", color="magenta", weight=3];
65 -> 2971[label="",style="dashed", color="magenta", weight=3];
65 -> 2972[label="",style="dashed", color="magenta", weight=3];
66[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat Zero Zero) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];66 -> 76[label="",style="solid", color="black", weight=3];
67[label="ceilingCeiling0 (Float (Neg (Succ yu3000)) (Neg (Succ yu3100))) (primCmpInt (Neg (primMulNat (primPlusNat (Succ yu3000) (primDivNatS (Succ yu3000) (Succ yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];67 -> 77[label="",style="solid", color="black", weight=3];
68[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg (primMulNat (primPlusNat Zero (primDivNatS Zero (Succ yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];68 -> 78[label="",style="solid", color="black", weight=3];
69[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu30000))) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) yu3100 (primGEqNatS (Succ yu30000) yu3100))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6216[label="yu3100/Succ yu31000",fontsize=10,color="white",style="solid",shape="box"];69 -> 6216[label="",style="solid", color="burlywood", weight=9];
6216 -> 79[label="",style="solid", color="burlywood", weight=3];
6217[label="yu3100/Zero",fontsize=10,color="white",style="solid",shape="box"];69 -> 6217[label="",style="solid", color="burlywood", weight=9];
6217 -> 80[label="",style="solid", color="burlywood", weight=3];
70[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu3100))) (primCmpInt (primMulInt (primMinusNat (Succ Zero) (primDivNatS0 Zero yu3100 (primGEqNatS Zero yu3100))) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="burlywood",shape="box"];6218[label="yu3100/Succ yu31000",fontsize=10,color="white",style="solid",shape="box"];70 -> 6218[label="",style="solid", color="burlywood", weight=9];
6218 -> 81[label="",style="solid", color="burlywood", weight=3];
6219[label="yu3100/Zero",fontsize=10,color="white",style="solid",shape="box"];70 -> 6219[label="",style="solid", color="burlywood", weight=9];
6219 -> 82[label="",style="solid", color="burlywood", weight=3];
71[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (primMulInt (Pos Zero) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];71 -> 83[label="",style="solid", color="black", weight=3];
72 -> 5858[label="",style="dashed", color="red", weight=0];
72[label="ceilingCeiling0 (Float (Pos (Succ yu3000)) (Neg (Succ yu3100))) (primCmpInt (Pos (primMulNat (primPlusNat (Succ yu3000) (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="magenta"];72 -> 5859[label="",style="dashed", color="magenta", weight=3];
72 -> 5860[label="",style="dashed", color="magenta", weight=3];
72 -> 5861[label="",style="dashed", color="magenta", weight=3];
73[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos (primMulNat (primPlusNat Zero Zero) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];73 -> 86[label="",style="solid", color="black", weight=3];
2970[label="yu3000",fontsize=16,color="green",shape="box"];2971 -> 4381[label="",style="dashed", color="red", weight=0];
2971[label="primMinusNat (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100)) (Succ yu3000)",fontsize=16,color="magenta"];2971 -> 4382[label="",style="dashed", color="magenta", weight=3];
2971 -> 4383[label="",style="dashed", color="magenta", weight=3];
2972[label="yu3100",fontsize=16,color="green",shape="box"];2969[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (primMulInt yu343 (Pos Zero)) (Pos (Succ yu243) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6222[label="yu343/Pos yu3430",fontsize=10,color="white",style="solid",shape="box"];2969 -> 6222[label="",style="solid", color="burlywood", weight=9];
6222 -> 3463[label="",style="solid", color="burlywood", weight=3];
6223[label="yu343/Neg yu3430",fontsize=10,color="white",style="solid",shape="box"];2969 -> 6223[label="",style="solid", color="burlywood", weight=9];
6223 -> 3464[label="",style="solid", color="burlywood", weight=3];
76[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (primMulInt (Pos Zero) (Pos Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];76 -> 91[label="",style="solid", color="black", weight=3];
77 -> 5908[label="",style="dashed", color="red", weight=0];
77[label="ceilingCeiling0 (Float (Neg (Succ yu3000)) (Neg (Succ yu3100))) (primCmpInt (Neg (primMulNat (primPlusNat (Succ yu3000) (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100))) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="magenta"];77 -> 5909[label="",style="dashed", color="magenta", weight=3];
77 -> 5910[label="",style="dashed", color="magenta", weight=3];
77 -> 5911[label="",style="dashed", color="magenta", weight=3];
78[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg (primMulNat (primPlusNat Zero Zero) Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];78 -> 94[label="",style="solid", color="black", weight=3];
79[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu30000))) (Pos (Succ (Succ yu31000)))) (primCmpInt (primMulInt (primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) (Succ yu31000) (primGEqNatS (Succ yu30000) (Succ yu31000)))) (Pos Zero)) (Pos (Succ (Succ yu31000)) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];79 -> 95[label="",style="solid", color="black", weight=3];
80[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu30000))) (Pos (Succ Zero))) (primCmpInt (primMulInt (primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) Zero (primGEqNatS (Succ yu30000) Zero))) (Pos Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];80 -> 96[label="",style="solid", color="black", weight=3];
81[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ (Succ yu31000)))) (primCmpInt (primMulInt (primMinusNat (Succ Zero) (primDivNatS0 Zero (Succ yu31000) (primGEqNatS Zero (Succ yu31000)))) (Pos Zero)) (Pos (Succ (Succ yu31000)) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];81 -> 97[label="",style="solid", color="black", weight=3];
82[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (primMulInt (primMinusNat (Succ Zero) (primDivNatS0 Zero Zero (primGEqNatS Zero Zero))) (Pos Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];82 -> 98[label="",style="solid", color="black", weight=3];
83[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (Pos (primMulNat Zero Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];83 -> 99[label="",style="solid", color="black", weight=3];
5859[label="yu3100",fontsize=16,color="green",shape="box"];5860 -> 5666[label="",style="dashed", color="red", weight=0];
5860[label="primPlusNat (Succ yu3000) (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100))",fontsize=16,color="magenta"];5860 -> 5863[label="",style="dashed", color="magenta", weight=3];
5860 -> 5864[label="",style="dashed", color="magenta", weight=3];
5861[label="yu3000",fontsize=16,color="green",shape="box"];5858[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (primCmpInt (Pos (primMulNat yu474 Zero)) (Neg (Succ yu471) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6226[label="yu474/Succ yu4740",fontsize=10,color="white",style="solid",shape="box"];5858 -> 6226[label="",style="solid", color="burlywood", weight=9];
6226 -> 5865[label="",style="solid", color="burlywood", weight=3];
6227[label="yu474/Zero",fontsize=10,color="white",style="solid",shape="box"];5858 -> 6227[label="",style="solid", color="burlywood", weight=9];
6227 -> 5866[label="",style="solid", color="burlywood", weight=3];
86[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos (primMulNat Zero Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];86 -> 104[label="",style="solid", color="black", weight=3];
4382[label="primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100)",fontsize=16,color="burlywood",shape="triangle"];6228[label="yu3000/Succ yu30000",fontsize=10,color="white",style="solid",shape="box"];4382 -> 6228[label="",style="solid", color="burlywood", weight=9];
6228 -> 4623[label="",style="solid", color="burlywood", weight=3];
6229[label="yu3000/Zero",fontsize=10,color="white",style="solid",shape="box"];4382 -> 6229[label="",style="solid", color="burlywood", weight=9];
6229 -> 4624[label="",style="solid", color="burlywood", weight=3];
4383[label="Succ yu3000",fontsize=16,color="green",shape="box"];4381[label="primMinusNat yu406 yu390",fontsize=16,color="burlywood",shape="triangle"];6230[label="yu406/Succ yu4060",fontsize=10,color="white",style="solid",shape="box"];4381 -> 6230[label="",style="solid", color="burlywood", weight=9];
6230 -> 4625[label="",style="solid", color="burlywood", weight=3];
6231[label="yu406/Zero",fontsize=10,color="white",style="solid",shape="box"];4381 -> 6231[label="",style="solid", color="burlywood", weight=9];
6231 -> 4626[label="",style="solid", color="burlywood", weight=3];
3463[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (primMulInt (Pos yu3430) (Pos Zero)) (Pos (Succ yu243) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3463 -> 3481[label="",style="solid", color="black", weight=3];
3464[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (primMulInt (Neg yu3430) (Pos Zero)) (Pos (Succ yu243) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3464 -> 3482[label="",style="solid", color="black", weight=3];
91[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (Pos (primMulNat Zero Zero)) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];91 -> 109[label="",style="solid", color="black", weight=3];
5909[label="yu3100",fontsize=16,color="green",shape="box"];5910[label="yu3000",fontsize=16,color="green",shape="box"];5911 -> 5666[label="",style="dashed", color="red", weight=0];
5911[label="primPlusNat (Succ yu3000) (primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100))",fontsize=16,color="magenta"];5911 -> 5913[label="",style="dashed", color="magenta", weight=3];
5911 -> 5914[label="",style="dashed", color="magenta", weight=3];
5908[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpInt (Neg (primMulNat yu480 Zero)) (Neg (Succ yu477) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6233[label="yu480/Succ yu4800",fontsize=10,color="white",style="solid",shape="box"];5908 -> 6233[label="",style="solid", color="burlywood", weight=9];
6233 -> 5915[label="",style="solid", color="burlywood", weight=3];
6234[label="yu480/Zero",fontsize=10,color="white",style="solid",shape="box"];5908 -> 6234[label="",style="solid", color="burlywood", weight=9];
6234 -> 5916[label="",style="solid", color="burlywood", weight=3];
94[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg (primMulNat Zero Zero)) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];94 -> 114[label="",style="solid", color="black", weight=3];
95 -> 5300[label="",style="dashed", color="red", weight=0];
95[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu30000))) (Pos (Succ (Succ yu31000)))) (primCmpInt (primMulInt (primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) (Succ yu31000) (primGEqNatS yu30000 yu31000))) (Pos Zero)) (Pos (Succ (Succ yu31000)) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="magenta"];95 -> 5301[label="",style="dashed", color="magenta", weight=3];
95 -> 5302[label="",style="dashed", color="magenta", weight=3];
95 -> 5303[label="",style="dashed", color="magenta", weight=3];
96 -> 5300[label="",style="dashed", color="red", weight=0];
96[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu30000))) (Pos (Succ Zero))) (primCmpInt (primMulInt (primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) Zero True)) (Pos Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="magenta"];96 -> 5304[label="",style="dashed", color="magenta", weight=3];
96 -> 5305[label="",style="dashed", color="magenta", weight=3];
96 -> 5306[label="",style="dashed", color="magenta", weight=3];
97 -> 3694[label="",style="dashed", color="red", weight=0];
97[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ (Succ yu31000)))) (primCmpInt (primMulInt (primMinusNat (Succ Zero) (primDivNatS0 Zero (Succ yu31000) False)) (Pos Zero)) (Pos (Succ (Succ yu31000)) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="magenta"];97 -> 3695[label="",style="dashed", color="magenta", weight=3];
97 -> 3696[label="",style="dashed", color="magenta", weight=3];
98 -> 3694[label="",style="dashed", color="red", weight=0];
98[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primCmpInt (primMulInt (primMinusNat (Succ Zero) (primDivNatS0 Zero Zero True)) (Pos Zero)) (Pos (Succ Zero) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="magenta"];98 -> 3697[label="",style="dashed", color="magenta", weight=3];
98 -> 3698[label="",style="dashed", color="magenta", weight=3];
99[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];99 -> 120[label="",style="solid", color="black", weight=3];
5863 -> 4382[label="",style="dashed", color="red", weight=0];
5863[label="primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100)",fontsize=16,color="magenta"];5863 -> 5917[label="",style="dashed", color="magenta", weight=3];
5863 -> 5918[label="",style="dashed", color="magenta", weight=3];
5864[label="Succ yu3000",fontsize=16,color="green",shape="box"];5666[label="primPlusNat yu30000000 yu434000",fontsize=16,color="burlywood",shape="triangle"];6240[label="yu30000000/Succ yu300000000",fontsize=10,color="white",style="solid",shape="box"];5666 -> 6240[label="",style="solid", color="burlywood", weight=9];
6240 -> 5697[label="",style="solid", color="burlywood", weight=3];
6241[label="yu30000000/Zero",fontsize=10,color="white",style="solid",shape="box"];5666 -> 6241[label="",style="solid", color="burlywood", weight=9];
6241 -> 5698[label="",style="solid", color="burlywood", weight=3];
5865[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (primCmpInt (Pos (primMulNat (Succ yu4740) Zero)) (Neg (Succ yu471) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5865 -> 5919[label="",style="solid", color="black", weight=3];
5866[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (primCmpInt (Pos (primMulNat Zero Zero)) (Neg (Succ yu471) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5866 -> 5920[label="",style="solid", color="black", weight=3];
104[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos Zero) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];104 -> 125[label="",style="solid", color="black", weight=3];
4623[label="primDivNatS0 (Succ yu30000) yu3100 (primGEqNatS (Succ yu30000) yu3100)",fontsize=16,color="burlywood",shape="box"];6242[label="yu3100/Succ yu31000",fontsize=10,color="white",style="solid",shape="box"];4623 -> 6242[label="",style="solid", color="burlywood", weight=9];
6242 -> 4643[label="",style="solid", color="burlywood", weight=3];
6243[label="yu3100/Zero",fontsize=10,color="white",style="solid",shape="box"];4623 -> 6243[label="",style="solid", color="burlywood", weight=9];
6243 -> 4644[label="",style="solid", color="burlywood", weight=3];
4624[label="primDivNatS0 Zero yu3100 (primGEqNatS Zero yu3100)",fontsize=16,color="burlywood",shape="box"];6244[label="yu3100/Succ yu31000",fontsize=10,color="white",style="solid",shape="box"];4624 -> 6244[label="",style="solid", color="burlywood", weight=9];
6244 -> 4645[label="",style="solid", color="burlywood", weight=3];
6245[label="yu3100/Zero",fontsize=10,color="white",style="solid",shape="box"];4624 -> 6245[label="",style="solid", color="burlywood", weight=9];
6245 -> 4646[label="",style="solid", color="burlywood", weight=3];
4625[label="primMinusNat (Succ yu4060) yu390",fontsize=16,color="burlywood",shape="box"];6246[label="yu390/Succ yu3900",fontsize=10,color="white",style="solid",shape="box"];4625 -> 6246[label="",style="solid", color="burlywood", weight=9];
6246 -> 4647[label="",style="solid", color="burlywood", weight=3];
6247[label="yu390/Zero",fontsize=10,color="white",style="solid",shape="box"];4625 -> 6247[label="",style="solid", color="burlywood", weight=9];
6247 -> 4648[label="",style="solid", color="burlywood", weight=3];
4626[label="primMinusNat Zero yu390",fontsize=16,color="burlywood",shape="box"];6248[label="yu390/Succ yu3900",fontsize=10,color="white",style="solid",shape="box"];4626 -> 6248[label="",style="solid", color="burlywood", weight=9];
6248 -> 4649[label="",style="solid", color="burlywood", weight=3];
6249[label="yu390/Zero",fontsize=10,color="white",style="solid",shape="box"];4626 -> 6249[label="",style="solid", color="burlywood", weight=9];
6249 -> 4650[label="",style="solid", color="burlywood", weight=3];
3481[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Pos (primMulNat yu3430 Zero)) (Pos (Succ yu243) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="box"];6250[label="yu3430/Succ yu34300",fontsize=10,color="white",style="solid",shape="box"];3481 -> 6250[label="",style="solid", color="burlywood", weight=9];
6250 -> 3496[label="",style="solid", color="burlywood", weight=3];
6251[label="yu3430/Zero",fontsize=10,color="white",style="solid",shape="box"];3481 -> 6251[label="",style="solid", color="burlywood", weight=9];
6251 -> 3497[label="",style="solid", color="burlywood", weight=3];
3482[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Neg (primMulNat yu3430 Zero)) (Pos (Succ yu243) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="box"];6252[label="yu3430/Succ yu34300",fontsize=10,color="white",style="solid",shape="box"];3482 -> 6252[label="",style="solid", color="burlywood", weight=9];
6252 -> 3498[label="",style="solid", color="burlywood", weight=3];
6253[label="yu3430/Zero",fontsize=10,color="white",style="solid",shape="box"];3482 -> 6253[label="",style="solid", color="burlywood", weight=9];
6253 -> 3499[label="",style="solid", color="burlywood", weight=3];
109[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (Pos (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];109 -> 131[label="",style="solid", color="black", weight=3];
5913 -> 4382[label="",style="dashed", color="red", weight=0];
5913[label="primDivNatS0 yu3000 yu3100 (primGEqNatS yu3000 yu3100)",fontsize=16,color="magenta"];5913 -> 5940[label="",style="dashed", color="magenta", weight=3];
5914[label="Succ yu3000",fontsize=16,color="green",shape="box"];5915[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpInt (Neg (primMulNat (Succ yu4800) Zero)) (Neg (Succ yu477) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5915 -> 5941[label="",style="solid", color="black", weight=3];
5916[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpInt (Neg (primMulNat Zero Zero)) (Neg (Succ yu477) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5916 -> 5942[label="",style="solid", color="black", weight=3];
114[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg Zero) (Neg (Succ yu3100) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)",fontsize=16,color="black",shape="box"];114 -> 136[label="",style="solid", color="black", weight=3];
5301[label="yu30000",fontsize=16,color="green",shape="box"];5302[label="Succ yu31000",fontsize=16,color="green",shape="box"];5303 -> 4381[label="",style="dashed", color="red", weight=0];
5303[label="primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) (Succ yu31000) (primGEqNatS yu30000 yu31000))",fontsize=16,color="magenta"];5303 -> 5620[label="",style="dashed", color="magenta", weight=3];
5303 -> 5621[label="",style="dashed", color="magenta", weight=3];
5300[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (primMulInt yu441 (Pos Zero)) (Pos (Succ yu320) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6256[label="yu441/Pos yu4410",fontsize=10,color="white",style="solid",shape="box"];5300 -> 6256[label="",style="solid", color="burlywood", weight=9];
6256 -> 5622[label="",style="solid", color="burlywood", weight=3];
6257[label="yu441/Neg yu4410",fontsize=10,color="white",style="solid",shape="box"];5300 -> 6257[label="",style="solid", color="burlywood", weight=9];
6257 -> 5623[label="",style="solid", color="burlywood", weight=3];
5304[label="yu30000",fontsize=16,color="green",shape="box"];5305[label="Zero",fontsize=16,color="green",shape="box"];5306 -> 4381[label="",style="dashed", color="red", weight=0];
5306[label="primMinusNat (Succ (Succ yu30000)) (primDivNatS0 (Succ yu30000) Zero True)",fontsize=16,color="magenta"];5306 -> 5624[label="",style="dashed", color="magenta", weight=3];
5306 -> 5625[label="",style="dashed", color="magenta", weight=3];
3695[label="Succ yu31000",fontsize=16,color="green",shape="box"];3696 -> 4381[label="",style="dashed", color="red", weight=0];
3696[label="primMinusNat (Succ Zero) (primDivNatS0 Zero (Succ yu31000) False)",fontsize=16,color="magenta"];3696 -> 4384[label="",style="dashed", color="magenta", weight=3];
3696 -> 4385[label="",style="dashed", color="magenta", weight=3];
3694[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (primMulInt yu362 (Pos Zero)) (Pos (Succ yu206) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6260[label="yu362/Pos yu3620",fontsize=10,color="white",style="solid",shape="box"];3694 -> 6260[label="",style="solid", color="burlywood", weight=9];
6260 -> 3725[label="",style="solid", color="burlywood", weight=3];
6261[label="yu362/Neg yu3620",fontsize=10,color="white",style="solid",shape="box"];3694 -> 6261[label="",style="solid", color="burlywood", weight=9];
6261 -> 3726[label="",style="solid", color="burlywood", weight=3];
3697[label="Zero",fontsize=16,color="green",shape="box"];3698 -> 4381[label="",style="dashed", color="red", weight=0];
3698[label="primMinusNat (Succ Zero) (primDivNatS0 Zero Zero True)",fontsize=16,color="magenta"];3698 -> 4386[label="",style="dashed", color="magenta", weight=3];
3698 -> 4387[label="",style="dashed", color="magenta", weight=3];
120[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (Pos (Succ yu3100) * Pos (Succ Zero)) (Pos (Succ Zero))) == GT)",fontsize=16,color="black",shape="box"];120 -> 144[label="",style="solid", color="black", weight=3];
5917[label="yu3100",fontsize=16,color="green",shape="box"];5918[label="yu3000",fontsize=16,color="green",shape="box"];5697[label="primPlusNat (Succ yu300000000) yu434000",fontsize=16,color="burlywood",shape="box"];6263[label="yu434000/Succ yu4340000",fontsize=10,color="white",style="solid",shape="box"];5697 -> 6263[label="",style="solid", color="burlywood", weight=9];
6263 -> 5714[label="",style="solid", color="burlywood", weight=3];
6264[label="yu434000/Zero",fontsize=10,color="white",style="solid",shape="box"];5697 -> 6264[label="",style="solid", color="burlywood", weight=9];
6264 -> 5715[label="",style="solid", color="burlywood", weight=3];
5698[label="primPlusNat Zero yu434000",fontsize=16,color="burlywood",shape="box"];6265[label="yu434000/Succ yu4340000",fontsize=10,color="white",style="solid",shape="box"];5698 -> 6265[label="",style="solid", color="burlywood", weight=9];
6265 -> 5716[label="",style="solid", color="burlywood", weight=3];
6266[label="yu434000/Zero",fontsize=10,color="white",style="solid",shape="box"];5698 -> 6266[label="",style="solid", color="burlywood", weight=9];
6266 -> 5717[label="",style="solid", color="burlywood", weight=3];
5919[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (primCmpInt (Pos Zero) (Neg (Succ yu471) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5919 -> 5943[label="",style="solid", color="black", weight=3];
5920 -> 5919[label="",style="dashed", color="red", weight=0];
5920[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (primCmpInt (Pos Zero) (Neg (Succ yu471) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="magenta"];125[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (Neg (Succ yu3100) * Pos (Succ Zero)) (Pos (Succ Zero))) == GT)",fontsize=16,color="black",shape="box"];125 -> 150[label="",style="solid", color="black", weight=3];
4643[label="primDivNatS0 (Succ yu30000) (Succ yu31000) (primGEqNatS (Succ yu30000) (Succ yu31000))",fontsize=16,color="black",shape="box"];4643 -> 4667[label="",style="solid", color="black", weight=3];
4644[label="primDivNatS0 (Succ yu30000) Zero (primGEqNatS (Succ yu30000) Zero)",fontsize=16,color="black",shape="box"];4644 -> 4668[label="",style="solid", color="black", weight=3];
4645[label="primDivNatS0 Zero (Succ yu31000) (primGEqNatS Zero (Succ yu31000))",fontsize=16,color="black",shape="box"];4645 -> 4669[label="",style="solid", color="black", weight=3];
4646[label="primDivNatS0 Zero Zero (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];4646 -> 4670[label="",style="solid", color="black", weight=3];
4647[label="primMinusNat (Succ yu4060) (Succ yu3900)",fontsize=16,color="black",shape="box"];4647 -> 4671[label="",style="solid", color="black", weight=3];
4648[label="primMinusNat (Succ yu4060) Zero",fontsize=16,color="black",shape="box"];4648 -> 4672[label="",style="solid", color="black", weight=3];
4649[label="primMinusNat Zero (Succ yu3900)",fontsize=16,color="black",shape="box"];4649 -> 4673[label="",style="solid", color="black", weight=3];
4650[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="box"];4650 -> 4674[label="",style="solid", color="black", weight=3];
3496[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Pos (primMulNat (Succ yu34300) Zero)) (Pos (Succ yu243) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3496 -> 3509[label="",style="solid", color="black", weight=3];
3497[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Pos (primMulNat Zero Zero)) (Pos (Succ yu243) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3497 -> 3510[label="",style="solid", color="black", weight=3];
3498[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Neg (primMulNat (Succ yu34300) Zero)) (Pos (Succ yu243) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3498 -> 3511[label="",style="solid", color="black", weight=3];
3499[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Neg (primMulNat Zero Zero)) (Pos (Succ yu243) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3499 -> 3512[label="",style="solid", color="black", weight=3];
131[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (Pos (Succ yu3100) * Pos (Succ Zero)) (Pos (Succ Zero))) == GT)",fontsize=16,color="black",shape="box"];131 -> 158[label="",style="solid", color="black", weight=3];
5940[label="yu3100",fontsize=16,color="green",shape="box"];5941[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpInt (Neg Zero) (Neg (Succ yu477) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5941 -> 5958[label="",style="solid", color="black", weight=3];
5942 -> 5941[label="",style="dashed", color="red", weight=0];
5942[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpInt (Neg Zero) (Neg (Succ yu477) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="magenta"];136[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg Zero) (primMulInt (Neg (Succ yu3100) * Pos (Succ Zero)) (Pos (Succ Zero))) == GT)",fontsize=16,color="black",shape="box"];136 -> 164[label="",style="solid", color="black", weight=3];
5620[label="Succ (Succ yu30000)",fontsize=16,color="green",shape="box"];5621 -> 6049[label="",style="dashed", color="red", weight=0];
5621[label="primDivNatS0 (Succ yu30000) (Succ yu31000) (primGEqNatS yu30000 yu31000)",fontsize=16,color="magenta"];5621 -> 6050[label="",style="dashed", color="magenta", weight=3];
5621 -> 6051[label="",style="dashed", color="magenta", weight=3];
5621 -> 6052[label="",style="dashed", color="magenta", weight=3];
5621 -> 6053[label="",style="dashed", color="magenta", weight=3];
5622[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (primMulInt (Pos yu4410) (Pos Zero)) (Pos (Succ yu320) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5622 -> 5642[label="",style="solid", color="black", weight=3];
5623[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (primMulInt (Neg yu4410) (Pos Zero)) (Pos (Succ yu320) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5623 -> 5643[label="",style="solid", color="black", weight=3];
5624[label="Succ (Succ yu30000)",fontsize=16,color="green",shape="box"];5625 -> 4883[label="",style="dashed", color="red", weight=0];
5625[label="primDivNatS0 (Succ yu30000) Zero True",fontsize=16,color="magenta"];5625 -> 5644[label="",style="dashed", color="magenta", weight=3];
5625 -> 5645[label="",style="dashed", color="magenta", weight=3];
4384[label="Succ Zero",fontsize=16,color="green",shape="box"];4385 -> 3662[label="",style="dashed", color="red", weight=0];
4385[label="primDivNatS0 Zero (Succ yu31000) False",fontsize=16,color="magenta"];3725[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (primMulInt (Pos yu3620) (Pos Zero)) (Pos (Succ yu206) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3725 -> 3760[label="",style="solid", color="black", weight=3];
3726[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (primMulInt (Neg yu3620) (Pos Zero)) (Pos (Succ yu206) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3726 -> 3761[label="",style="solid", color="black", weight=3];
4386[label="Succ Zero",fontsize=16,color="green",shape="box"];4387[label="primDivNatS0 Zero Zero True",fontsize=16,color="black",shape="triangle"];4387 -> 4627[label="",style="solid", color="black", weight=3];
144[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Pos (Succ yu3100)) (Pos (Succ Zero))) (Pos (Succ Zero))) == GT)",fontsize=16,color="black",shape="box"];144 -> 172[label="",style="solid", color="black", weight=3];
5714[label="primPlusNat (Succ yu300000000) (Succ yu4340000)",fontsize=16,color="black",shape="box"];5714 -> 5921[label="",style="solid", color="black", weight=3];
5715[label="primPlusNat (Succ yu300000000) Zero",fontsize=16,color="black",shape="box"];5715 -> 5922[label="",style="solid", color="black", weight=3];
5716[label="primPlusNat Zero (Succ yu4340000)",fontsize=16,color="black",shape="box"];5716 -> 5923[label="",style="solid", color="black", weight=3];
5717[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];5717 -> 5924[label="",style="solid", color="black", weight=3];
5943[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (primCmpInt (Pos Zero) (primMulInt (Neg (Succ yu471) * Pos (Succ Zero)) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5943 -> 5959[label="",style="solid", color="black", weight=3];
150[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Neg (Succ yu3100)) (Pos (Succ Zero))) (Pos (Succ Zero))) == GT)",fontsize=16,color="black",shape="box"];150 -> 180[label="",style="solid", color="black", weight=3];
4667 -> 6049[label="",style="dashed", color="red", weight=0];
4667[label="primDivNatS0 (Succ yu30000) (Succ yu31000) (primGEqNatS yu30000 yu31000)",fontsize=16,color="magenta"];4667 -> 6054[label="",style="dashed", color="magenta", weight=3];
4667 -> 6055[label="",style="dashed", color="magenta", weight=3];
4667 -> 6056[label="",style="dashed", color="magenta", weight=3];
4667 -> 6057[label="",style="dashed", color="magenta", weight=3];
4668 -> 4883[label="",style="dashed", color="red", weight=0];
4668[label="primDivNatS0 (Succ yu30000) Zero True",fontsize=16,color="magenta"];4668 -> 4884[label="",style="dashed", color="magenta", weight=3];
4668 -> 4885[label="",style="dashed", color="magenta", weight=3];
4669 -> 3662[label="",style="dashed", color="red", weight=0];
4669[label="primDivNatS0 Zero (Succ yu31000) False",fontsize=16,color="magenta"];4670 -> 4387[label="",style="dashed", color="red", weight=0];
4670[label="primDivNatS0 Zero Zero True",fontsize=16,color="magenta"];4671 -> 4381[label="",style="dashed", color="red", weight=0];
4671[label="primMinusNat yu4060 yu3900",fontsize=16,color="magenta"];4671 -> 4700[label="",style="dashed", color="magenta", weight=3];
4671 -> 4701[label="",style="dashed", color="magenta", weight=3];
4672[label="Pos (Succ yu4060)",fontsize=16,color="green",shape="box"];4673[label="Neg (Succ yu3900)",fontsize=16,color="green",shape="box"];4674[label="Pos Zero",fontsize=16,color="green",shape="box"];3509[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Pos Zero) (Pos (Succ yu243) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3509 -> 3524[label="",style="solid", color="black", weight=3];
3510 -> 3509[label="",style="dashed", color="red", weight=0];
3510[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Pos Zero) (Pos (Succ yu243) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="magenta"];3511[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Neg Zero) (Pos (Succ yu243) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3511 -> 3525[label="",style="solid", color="black", weight=3];
3512 -> 3511[label="",style="dashed", color="red", weight=0];
3512[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Neg Zero) (Pos (Succ yu243) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="magenta"];158[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Pos (Succ yu3100)) (Pos (Succ Zero))) (Pos (Succ Zero))) == GT)",fontsize=16,color="black",shape="box"];158 -> 188[label="",style="solid", color="black", weight=3];
5958[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpInt (Neg Zero) (primMulInt (Neg (Succ yu477) * Pos (Succ Zero)) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5958 -> 5971[label="",style="solid", color="black", weight=3];
164[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg Zero) (primMulInt (primMulInt (Neg (Succ yu3100)) (Pos (Succ Zero))) (Pos (Succ Zero))) == GT)",fontsize=16,color="black",shape="box"];164 -> 196[label="",style="solid", color="black", weight=3];
6050[label="yu31000",fontsize=16,color="green",shape="box"];6051[label="yu30000",fontsize=16,color="green",shape="box"];6052[label="yu30000",fontsize=16,color="green",shape="box"];6053[label="yu31000",fontsize=16,color="green",shape="box"];6049[label="primDivNatS0 (Succ yu494) (Succ yu495) (primGEqNatS yu496 yu497)",fontsize=16,color="burlywood",shape="triangle"];6279[label="yu496/Succ yu4960",fontsize=10,color="white",style="solid",shape="box"];6049 -> 6279[label="",style="solid", color="burlywood", weight=9];
6279 -> 6098[label="",style="solid", color="burlywood", weight=3];
6280[label="yu496/Zero",fontsize=10,color="white",style="solid",shape="box"];6049 -> 6280[label="",style="solid", color="burlywood", weight=9];
6280 -> 6099[label="",style="solid", color="burlywood", weight=3];
5642[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Pos (primMulNat yu4410 Zero)) (Pos (Succ yu320) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="box"];6281[label="yu4410/Succ yu44100",fontsize=10,color="white",style="solid",shape="box"];5642 -> 6281[label="",style="solid", color="burlywood", weight=9];
6281 -> 5657[label="",style="solid", color="burlywood", weight=3];
6282[label="yu4410/Zero",fontsize=10,color="white",style="solid",shape="box"];5642 -> 6282[label="",style="solid", color="burlywood", weight=9];
6282 -> 5658[label="",style="solid", color="burlywood", weight=3];
5643 -> 4746[label="",style="dashed", color="red", weight=0];
5643[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Neg (primMulNat yu4410 Zero)) (Pos (Succ yu320) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="magenta"];5643 -> 5659[label="",style="dashed", color="magenta", weight=3];
5643 -> 5660[label="",style="dashed", color="magenta", weight=3];
5643 -> 5661[label="",style="dashed", color="magenta", weight=3];
5644[label="Zero",fontsize=16,color="green",shape="box"];5645[label="yu30000",fontsize=16,color="green",shape="box"];4883[label="primDivNatS0 (Succ yu424) yu425 True",fontsize=16,color="black",shape="triangle"];4883 -> 4910[label="",style="solid", color="black", weight=3];
3662[label="primDivNatS0 Zero (Succ yu31000) False",fontsize=16,color="black",shape="triangle"];3662 -> 3669[label="",style="solid", color="black", weight=3];
3760[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Pos (primMulNat yu3620 Zero)) (Pos (Succ yu206) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="box"];6284[label="yu3620/Succ yu36200",fontsize=10,color="white",style="solid",shape="box"];3760 -> 6284[label="",style="solid", color="burlywood", weight=9];
6284 -> 3790[label="",style="solid", color="burlywood", weight=3];
6285[label="yu3620/Zero",fontsize=10,color="white",style="solid",shape="box"];3760 -> 6285[label="",style="solid", color="burlywood", weight=9];
6285 -> 3791[label="",style="solid", color="burlywood", weight=3];
3761 -> 4746[label="",style="dashed", color="red", weight=0];
3761[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Neg (primMulNat yu3620 Zero)) (Pos (Succ yu206) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="magenta"];3761 -> 4747[label="",style="dashed", color="magenta", weight=3];
3761 -> 4748[label="",style="dashed", color="magenta", weight=3];
3761 -> 4749[label="",style="dashed", color="magenta", weight=3];
4627[label="Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];4627 -> 4651[label="",style="dashed", color="green", weight=3];
172[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (Pos (primMulNat (Succ yu3100) (Succ Zero))) (Pos (Succ Zero))) == GT)",fontsize=16,color="black",shape="box"];172 -> 205[label="",style="solid", color="black", weight=3];
5921[label="Succ (Succ (primPlusNat yu300000000 yu4340000))",fontsize=16,color="green",shape="box"];5921 -> 5944[label="",style="dashed", color="green", weight=3];
5922[label="Succ yu300000000",fontsize=16,color="green",shape="box"];5923[label="Succ yu4340000",fontsize=16,color="green",shape="box"];5924[label="Zero",fontsize=16,color="green",shape="box"];5959[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Neg (Succ yu471)) (Pos (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5959 -> 5972[label="",style="solid", color="black", weight=3];
180[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (Neg (primMulNat (Succ yu3100) (Succ Zero))) (Pos (Succ Zero))) == GT)",fontsize=16,color="black",shape="box"];180 -> 213[label="",style="solid", color="black", weight=3];
6054[label="yu31000",fontsize=16,color="green",shape="box"];6055[label="yu30000",fontsize=16,color="green",shape="box"];6056[label="yu30000",fontsize=16,color="green",shape="box"];6057[label="yu31000",fontsize=16,color="green",shape="box"];4884[label="Zero",fontsize=16,color="green",shape="box"];4885[label="yu30000",fontsize=16,color="green",shape="box"];4700[label="yu4060",fontsize=16,color="green",shape="box"];4701[label="yu3900",fontsize=16,color="green",shape="box"];3524[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Pos Zero) (primMulInt (Pos (Succ yu243) * Pos (Succ Zero)) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3524 -> 3539[label="",style="solid", color="black", weight=3];
3525[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Neg Zero) (primMulInt (Pos (Succ yu243) * Pos (Succ Zero)) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3525 -> 3540[label="",style="solid", color="black", weight=3];
188[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (primMulInt (Pos (primMulNat (Succ yu3100) (Succ Zero))) (Pos (Succ Zero))) == GT)",fontsize=16,color="black",shape="box"];188 -> 222[label="",style="solid", color="black", weight=3];
5971[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpInt (Neg Zero) (primMulInt (primMulInt (Neg (Succ yu477)) (Pos (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5971 -> 5983[label="",style="solid", color="black", weight=3];
196[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg Zero) (primMulInt (Neg (primMulNat (Succ yu3100) (Succ Zero))) (Pos (Succ Zero))) == GT)",fontsize=16,color="black",shape="box"];196 -> 230[label="",style="solid", color="black", weight=3];
6098[label="primDivNatS0 (Succ yu494) (Succ yu495) (primGEqNatS (Succ yu4960) yu497)",fontsize=16,color="burlywood",shape="box"];6287[label="yu497/Succ yu4970",fontsize=10,color="white",style="solid",shape="box"];6098 -> 6287[label="",style="solid", color="burlywood", weight=9];
6287 -> 6110[label="",style="solid", color="burlywood", weight=3];
6288[label="yu497/Zero",fontsize=10,color="white",style="solid",shape="box"];6098 -> 6288[label="",style="solid", color="burlywood", weight=9];
6288 -> 6111[label="",style="solid", color="burlywood", weight=3];
6099[label="primDivNatS0 (Succ yu494) (Succ yu495) (primGEqNatS Zero yu497)",fontsize=16,color="burlywood",shape="box"];6289[label="yu497/Succ yu4970",fontsize=10,color="white",style="solid",shape="box"];6099 -> 6289[label="",style="solid", color="burlywood", weight=9];
6289 -> 6112[label="",style="solid", color="burlywood", weight=3];
6290[label="yu497/Zero",fontsize=10,color="white",style="solid",shape="box"];6099 -> 6290[label="",style="solid", color="burlywood", weight=9];
6290 -> 6113[label="",style="solid", color="burlywood", weight=3];
5657[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Pos (primMulNat (Succ yu44100) Zero)) (Pos (Succ yu320) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5657 -> 5672[label="",style="solid", color="black", weight=3];
5658[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Pos (primMulNat Zero Zero)) (Pos (Succ yu320) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5658 -> 5673[label="",style="solid", color="black", weight=3];
5659[label="yu4410",fontsize=16,color="green",shape="box"];5660[label="yu320",fontsize=16,color="green",shape="box"];5661[label="Succ yu3190",fontsize=16,color="green",shape="box"];4746[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (primCmpInt (Neg (primMulNat yu419 Zero)) (Pos (Succ yu418) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6291[label="yu419/Succ yu4190",fontsize=10,color="white",style="solid",shape="box"];4746 -> 6291[label="",style="solid", color="burlywood", weight=9];
6291 -> 4762[label="",style="solid", color="burlywood", weight=3];
6292[label="yu419/Zero",fontsize=10,color="white",style="solid",shape="box"];4746 -> 6292[label="",style="solid", color="burlywood", weight=9];
6292 -> 4763[label="",style="solid", color="burlywood", weight=3];
4910[label="Succ (primDivNatS (primMinusNatS (Succ yu424) yu425) (Succ yu425))",fontsize=16,color="green",shape="box"];4910 -> 4950[label="",style="dashed", color="green", weight=3];
3669[label="Zero",fontsize=16,color="green",shape="box"];3790[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Pos (primMulNat (Succ yu36200) Zero)) (Pos (Succ yu206) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3790 -> 3842[label="",style="solid", color="black", weight=3];
3791[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Pos (primMulNat Zero Zero)) (Pos (Succ yu206) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3791 -> 3843[label="",style="solid", color="black", weight=3];
4747[label="yu3620",fontsize=16,color="green",shape="box"];4748[label="yu206",fontsize=16,color="green",shape="box"];4749[label="Zero",fontsize=16,color="green",shape="box"];4651 -> 5998[label="",style="dashed", color="red", weight=0];
4651[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];4651 -> 5999[label="",style="dashed", color="magenta", weight=3];
4651 -> 6000[label="",style="dashed", color="magenta", weight=3];
4651 -> 6001[label="",style="dashed", color="magenta", weight=3];
205 -> 1460[label="",style="dashed", color="red", weight=0];
205[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (Pos (primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero))) == GT)",fontsize=16,color="magenta"];205 -> 1461[label="",style="dashed", color="magenta", weight=3];
205 -> 1462[label="",style="dashed", color="magenta", weight=3];
5944 -> 5666[label="",style="dashed", color="red", weight=0];
5944[label="primPlusNat yu300000000 yu4340000",fontsize=16,color="magenta"];5944 -> 5960[label="",style="dashed", color="magenta", weight=3];
5944 -> 5961[label="",style="dashed", color="magenta", weight=3];
5972 -> 5984[label="",style="dashed", color="red", weight=0];
5972[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (primCmpInt (Pos Zero) (primMulInt (Neg (primMulNat (Succ yu471) (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];5972 -> 5985[label="",style="dashed", color="magenta", weight=3];
213 -> 1595[label="",style="dashed", color="red", weight=0];
213[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu3100))) (primCmpInt (Pos Zero) (Neg (primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero))) == GT)",fontsize=16,color="magenta"];213 -> 1596[label="",style="dashed", color="magenta", weight=3];
213 -> 1597[label="",style="dashed", color="magenta", weight=3];
3539[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Pos (Succ yu243)) (Pos (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3539 -> 3591[label="",style="solid", color="black", weight=3];
3540[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Neg Zero) (primMulInt (primMulInt (Pos (Succ yu243)) (Pos (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3540 -> 3592[label="",style="solid", color="black", weight=3];
222 -> 1793[label="",style="dashed", color="red", weight=0];
222[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu3100))) (primCmpInt (Pos Zero) (Pos (primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero))) == GT)",fontsize=16,color="magenta"];222 -> 1794[label="",style="dashed", color="magenta", weight=3];
222 -> 1795[label="",style="dashed", color="magenta", weight=3];
5983 -> 5986[label="",style="dashed", color="red", weight=0];
5983[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpInt (Neg Zero) (primMulInt (Neg (primMulNat (Succ yu477) (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];5983 -> 5987[label="",style="dashed", color="magenta", weight=3];
230 -> 1981[label="",style="dashed", color="red", weight=0];
230[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu3100))) (primCmpInt (Neg Zero) (Neg (primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero))) == GT)",fontsize=16,color="magenta"];230 -> 1982[label="",style="dashed", color="magenta", weight=3];
230 -> 1983[label="",style="dashed", color="magenta", weight=3];
6110[label="primDivNatS0 (Succ yu494) (Succ yu495) (primGEqNatS (Succ yu4960) (Succ yu4970))",fontsize=16,color="black",shape="box"];6110 -> 6118[label="",style="solid", color="black", weight=3];
6111[label="primDivNatS0 (Succ yu494) (Succ yu495) (primGEqNatS (Succ yu4960) Zero)",fontsize=16,color="black",shape="box"];6111 -> 6119[label="",style="solid", color="black", weight=3];
6112[label="primDivNatS0 (Succ yu494) (Succ yu495) (primGEqNatS Zero (Succ yu4970))",fontsize=16,color="black",shape="box"];6112 -> 6120[label="",style="solid", color="black", weight=3];
6113[label="primDivNatS0 (Succ yu494) (Succ yu495) (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];6113 -> 6121[label="",style="solid", color="black", weight=3];
5672[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Pos Zero) (Pos (Succ yu320) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5672 -> 5689[label="",style="solid", color="black", weight=3];
5673 -> 5672[label="",style="dashed", color="red", weight=0];
5673[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Pos Zero) (Pos (Succ yu320) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="magenta"];4762[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (primCmpInt (Neg (primMulNat (Succ yu4190) Zero)) (Pos (Succ yu418) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];4762 -> 4824[label="",style="solid", color="black", weight=3];
4763[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (primCmpInt (Neg (primMulNat Zero Zero)) (Pos (Succ yu418) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];4763 -> 4825[label="",style="solid", color="black", weight=3];
4950 -> 5998[label="",style="dashed", color="red", weight=0];
4950[label="primDivNatS (primMinusNatS (Succ yu424) yu425) (Succ yu425)",fontsize=16,color="magenta"];4950 -> 6002[label="",style="dashed", color="magenta", weight=3];
4950 -> 6003[label="",style="dashed", color="magenta", weight=3];
4950 -> 6004[label="",style="dashed", color="magenta", weight=3];
3842[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Pos Zero) (Pos (Succ yu206) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3842 -> 3856[label="",style="solid", color="black", weight=3];
3843 -> 3842[label="",style="dashed", color="red", weight=0];
3843[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Pos Zero) (Pos (Succ yu206) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="magenta"];5999[label="Zero",fontsize=16,color="green",shape="box"];6000[label="Zero",fontsize=16,color="green",shape="box"];6001[label="Zero",fontsize=16,color="green",shape="box"];5998[label="primDivNatS (primMinusNatS yu488 yu489) (Succ yu490)",fontsize=16,color="burlywood",shape="triangle"];6304[label="yu488/Succ yu4880",fontsize=10,color="white",style="solid",shape="box"];5998 -> 6304[label="",style="solid", color="burlywood", weight=9];
6304 -> 6029[label="",style="solid", color="burlywood", weight=3];
6305[label="yu488/Zero",fontsize=10,color="white",style="solid",shape="box"];5998 -> 6305[label="",style="solid", color="burlywood", weight=9];
6305 -> 6030[label="",style="solid", color="burlywood", weight=3];
1461[label="yu3100",fontsize=16,color="green",shape="box"];1462 -> 1618[label="",style="dashed", color="red", weight=0];
1462[label="primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];1462 -> 1619[label="",style="dashed", color="magenta", weight=3];
1460[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu71))) (primCmpInt (Pos Zero) (Pos yu102) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6307[label="yu102/Succ yu1020",fontsize=10,color="white",style="solid",shape="box"];1460 -> 6307[label="",style="solid", color="burlywood", weight=9];
6307 -> 1479[label="",style="solid", color="burlywood", weight=3];
6308[label="yu102/Zero",fontsize=10,color="white",style="solid",shape="box"];1460 -> 6308[label="",style="solid", color="burlywood", weight=9];
6308 -> 1480[label="",style="solid", color="burlywood", weight=3];
5960[label="yu4340000",fontsize=16,color="green",shape="box"];5961[label="yu300000000",fontsize=16,color="green",shape="box"];5985 -> 1618[label="",style="dashed", color="red", weight=0];
5985[label="primMulNat (Succ yu471) (Succ Zero)",fontsize=16,color="magenta"];5985 -> 5988[label="",style="dashed", color="magenta", weight=3];
5984[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (primCmpInt (Pos Zero) (primMulInt (Neg yu485) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5984 -> 5989[label="",style="solid", color="black", weight=3];
1596[label="yu3100",fontsize=16,color="green",shape="box"];1597 -> 1618[label="",style="dashed", color="red", weight=0];
1597[label="primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];1597 -> 1620[label="",style="dashed", color="magenta", weight=3];
1595[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu78))) (primCmpInt (Pos Zero) (Neg yu112) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6311[label="yu112/Succ yu1120",fontsize=10,color="white",style="solid",shape="box"];1595 -> 6311[label="",style="solid", color="burlywood", weight=9];
6311 -> 1614[label="",style="solid", color="burlywood", weight=3];
6312[label="yu112/Zero",fontsize=10,color="white",style="solid",shape="box"];1595 -> 6312[label="",style="solid", color="burlywood", weight=9];
6312 -> 1615[label="",style="solid", color="burlywood", weight=3];
3591 -> 3617[label="",style="dashed", color="red", weight=0];
3591[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Pos Zero) (primMulInt (Pos (primMulNat (Succ yu243) (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];3591 -> 3618[label="",style="dashed", color="magenta", weight=3];
3592 -> 3619[label="",style="dashed", color="red", weight=0];
3592[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Neg Zero) (primMulInt (Pos (primMulNat (Succ yu243) (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];3592 -> 3620[label="",style="dashed", color="magenta", weight=3];
1794 -> 1618[label="",style="dashed", color="red", weight=0];
1794[label="primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];1794 -> 1861[label="",style="dashed", color="magenta", weight=3];
1795[label="yu3100",fontsize=16,color="green",shape="box"];1793[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu87))) (primCmpInt (Pos Zero) (Pos yu152) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6316[label="yu152/Succ yu1520",fontsize=10,color="white",style="solid",shape="box"];1793 -> 6316[label="",style="solid", color="burlywood", weight=9];
6316 -> 1862[label="",style="solid", color="burlywood", weight=3];
6317[label="yu152/Zero",fontsize=10,color="white",style="solid",shape="box"];1793 -> 6317[label="",style="solid", color="burlywood", weight=9];
6317 -> 1863[label="",style="solid", color="burlywood", weight=3];
5987 -> 1618[label="",style="dashed", color="red", weight=0];
5987[label="primMulNat (Succ yu477) (Succ Zero)",fontsize=16,color="magenta"];5987 -> 5990[label="",style="dashed", color="magenta", weight=3];
5986[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpInt (Neg Zero) (primMulInt (Neg yu486) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5986 -> 5991[label="",style="solid", color="black", weight=3];
1982[label="yu3100",fontsize=16,color="green",shape="box"];1983 -> 1618[label="",style="dashed", color="red", weight=0];
1983[label="primMulNat (primMulNat (Succ yu3100) (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];1983 -> 2049[label="",style="dashed", color="magenta", weight=3];
1981[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu94))) (primCmpInt (Neg Zero) (Neg yu196) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6320[label="yu196/Succ yu1960",fontsize=10,color="white",style="solid",shape="box"];1981 -> 6320[label="",style="solid", color="burlywood", weight=9];
6320 -> 2050[label="",style="solid", color="burlywood", weight=3];
6321[label="yu196/Zero",fontsize=10,color="white",style="solid",shape="box"];1981 -> 6321[label="",style="solid", color="burlywood", weight=9];
6321 -> 2051[label="",style="solid", color="burlywood", weight=3];
6118 -> 6049[label="",style="dashed", color="red", weight=0];
6118[label="primDivNatS0 (Succ yu494) (Succ yu495) (primGEqNatS yu4960 yu4970)",fontsize=16,color="magenta"];6118 -> 6126[label="",style="dashed", color="magenta", weight=3];
6118 -> 6127[label="",style="dashed", color="magenta", weight=3];
6119 -> 4883[label="",style="dashed", color="red", weight=0];
6119[label="primDivNatS0 (Succ yu494) (Succ yu495) True",fontsize=16,color="magenta"];6119 -> 6128[label="",style="dashed", color="magenta", weight=3];
6119 -> 6129[label="",style="dashed", color="magenta", weight=3];
6120[label="primDivNatS0 (Succ yu494) (Succ yu495) False",fontsize=16,color="black",shape="box"];6120 -> 6130[label="",style="solid", color="black", weight=3];
6121 -> 4883[label="",style="dashed", color="red", weight=0];
6121[label="primDivNatS0 (Succ yu494) (Succ yu495) True",fontsize=16,color="magenta"];6121 -> 6131[label="",style="dashed", color="magenta", weight=3];
6121 -> 6132[label="",style="dashed", color="magenta", weight=3];
5689[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Pos Zero) (primMulInt (Pos (Succ yu320) * Pos (Succ Zero)) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5689 -> 5701[label="",style="solid", color="black", weight=3];
4824[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (primCmpInt (Neg Zero) (Pos (Succ yu418) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];4824 -> 4864[label="",style="solid", color="black", weight=3];
4825 -> 4824[label="",style="dashed", color="red", weight=0];
4825[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (primCmpInt (Neg Zero) (Pos (Succ yu418) * Pos (Succ Zero) * Pos (Succ Zero)) == GT)\n  Integral a",fontsize=16,color="magenta"];6002[label="yu425",fontsize=16,color="green",shape="box"];6003[label="yu425",fontsize=16,color="green",shape="box"];6004[label="Succ yu424",fontsize=16,color="green",shape="box"];3856[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Pos Zero) (primMulInt (Pos (Succ yu206) * Pos (Succ Zero)) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3856 -> 3876[label="",style="solid", color="black", weight=3];
6029[label="primDivNatS (primMinusNatS (Succ yu4880) yu489) (Succ yu490)",fontsize=16,color="burlywood",shape="box"];6326[label="yu489/Succ yu4890",fontsize=10,color="white",style="solid",shape="box"];6029 -> 6326[label="",style="solid", color="burlywood", weight=9];
6326 -> 6033[label="",style="solid", color="burlywood", weight=3];
6327[label="yu489/Zero",fontsize=10,color="white",style="solid",shape="box"];6029 -> 6327[label="",style="solid", color="burlywood", weight=9];
6327 -> 6034[label="",style="solid", color="burlywood", weight=3];
6030[label="primDivNatS (primMinusNatS Zero yu489) (Succ yu490)",fontsize=16,color="burlywood",shape="box"];6328[label="yu489/Succ yu4890",fontsize=10,color="white",style="solid",shape="box"];6030 -> 6328[label="",style="solid", color="burlywood", weight=9];
6328 -> 6035[label="",style="solid", color="burlywood", weight=3];
6329[label="yu489/Zero",fontsize=10,color="white",style="solid",shape="box"];6030 -> 6329[label="",style="solid", color="burlywood", weight=9];
6329 -> 6036[label="",style="solid", color="burlywood", weight=3];
1619 -> 1618[label="",style="dashed", color="red", weight=0];
1619[label="primMulNat (Succ yu3100) (Succ Zero)",fontsize=16,color="magenta"];1619 -> 1635[label="",style="dashed", color="magenta", weight=3];
1618[label="primMulNat yu113 (Succ Zero)",fontsize=16,color="burlywood",shape="triangle"];6331[label="yu113/Succ yu1130",fontsize=10,color="white",style="solid",shape="box"];1618 -> 6331[label="",style="solid", color="burlywood", weight=9];
6331 -> 1636[label="",style="solid", color="burlywood", weight=3];
6332[label="yu113/Zero",fontsize=10,color="white",style="solid",shape="box"];1618 -> 6332[label="",style="solid", color="burlywood", weight=9];
6332 -> 1637[label="",style="solid", color="burlywood", weight=3];
1479[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu71))) (primCmpInt (Pos Zero) (Pos (Succ yu1020)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1479 -> 1485[label="",style="solid", color="black", weight=3];
1480[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu71))) (primCmpInt (Pos Zero) (Pos Zero) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1480 -> 1486[label="",style="solid", color="black", weight=3];
5988[label="Succ yu471",fontsize=16,color="green",shape="box"];5989 -> 6031[label="",style="dashed", color="red", weight=0];
5989[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (primCmpInt (Pos Zero) (Neg (primMulNat yu485 (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];5989 -> 6032[label="",style="dashed", color="magenta", weight=3];
1620 -> 1618[label="",style="dashed", color="red", weight=0];
1620[label="primMulNat (Succ yu3100) (Succ Zero)",fontsize=16,color="magenta"];1620 -> 1638[label="",style="dashed", color="magenta", weight=3];
1614[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu78))) (primCmpInt (Pos Zero) (Neg (Succ yu1120)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1614 -> 1639[label="",style="solid", color="black", weight=3];
1615[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu78))) (primCmpInt (Pos Zero) (Neg Zero) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1615 -> 1640[label="",style="solid", color="black", weight=3];
3618 -> 1618[label="",style="dashed", color="red", weight=0];
3618[label="primMulNat (Succ yu243) (Succ Zero)",fontsize=16,color="magenta"];3618 -> 3627[label="",style="dashed", color="magenta", weight=3];
3617[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Pos Zero) (primMulInt (Pos yu354) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3617 -> 3628[label="",style="solid", color="black", weight=3];
3620 -> 1618[label="",style="dashed", color="red", weight=0];
3620[label="primMulNat (Succ yu243) (Succ Zero)",fontsize=16,color="magenta"];3620 -> 3629[label="",style="dashed", color="magenta", weight=3];
3619[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Neg Zero) (primMulInt (Pos yu355) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3619 -> 3630[label="",style="solid", color="black", weight=3];
1861 -> 1618[label="",style="dashed", color="red", weight=0];
1861[label="primMulNat (Succ yu3100) (Succ Zero)",fontsize=16,color="magenta"];1861 -> 1878[label="",style="dashed", color="magenta", weight=3];
1862[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu87))) (primCmpInt (Pos Zero) (Pos (Succ yu1520)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1862 -> 1879[label="",style="solid", color="black", weight=3];
1863[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu87))) (primCmpInt (Pos Zero) (Pos Zero) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1863 -> 1880[label="",style="solid", color="black", weight=3];
5990[label="Succ yu477",fontsize=16,color="green",shape="box"];5991 -> 6037[label="",style="dashed", color="red", weight=0];
5991[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpInt (Neg Zero) (Neg (primMulNat yu486 (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];5991 -> 6038[label="",style="dashed", color="magenta", weight=3];
2049 -> 1618[label="",style="dashed", color="red", weight=0];
2049[label="primMulNat (Succ yu3100) (Succ Zero)",fontsize=16,color="magenta"];2049 -> 2072[label="",style="dashed", color="magenta", weight=3];
2050[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu94))) (primCmpInt (Neg Zero) (Neg (Succ yu1960)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];2050 -> 2073[label="",style="solid", color="black", weight=3];
2051[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu94))) (primCmpInt (Neg Zero) (Neg Zero) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];2051 -> 2074[label="",style="solid", color="black", weight=3];
6126[label="yu4970",fontsize=16,color="green",shape="box"];6127[label="yu4960",fontsize=16,color="green",shape="box"];6128[label="Succ yu495",fontsize=16,color="green",shape="box"];6129[label="yu494",fontsize=16,color="green",shape="box"];6130[label="Zero",fontsize=16,color="green",shape="box"];6131[label="Succ yu495",fontsize=16,color="green",shape="box"];6132[label="yu494",fontsize=16,color="green",shape="box"];5701[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Pos (Succ yu320)) (Pos (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5701 -> 5731[label="",style="solid", color="black", weight=3];
4864[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (primCmpInt (Neg Zero) (primMulInt (Pos (Succ yu418) * Pos (Succ Zero)) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];4864 -> 4911[label="",style="solid", color="black", weight=3];
3876[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Pos Zero) (primMulInt (primMulInt (Pos (Succ yu206)) (Pos (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3876 -> 3899[label="",style="solid", color="black", weight=3];
6033[label="primDivNatS (primMinusNatS (Succ yu4880) (Succ yu4890)) (Succ yu490)",fontsize=16,color="black",shape="box"];6033 -> 6039[label="",style="solid", color="black", weight=3];
6034[label="primDivNatS (primMinusNatS (Succ yu4880) Zero) (Succ yu490)",fontsize=16,color="black",shape="box"];6034 -> 6040[label="",style="solid", color="black", weight=3];
6035[label="primDivNatS (primMinusNatS Zero (Succ yu4890)) (Succ yu490)",fontsize=16,color="black",shape="box"];6035 -> 6041[label="",style="solid", color="black", weight=3];
6036[label="primDivNatS (primMinusNatS Zero Zero) (Succ yu490)",fontsize=16,color="black",shape="box"];6036 -> 6042[label="",style="solid", color="black", weight=3];
1635[label="Succ yu3100",fontsize=16,color="green",shape="box"];1636[label="primMulNat (Succ yu1130) (Succ Zero)",fontsize=16,color="black",shape="box"];1636 -> 1655[label="",style="solid", color="black", weight=3];
1637[label="primMulNat Zero (Succ Zero)",fontsize=16,color="black",shape="box"];1637 -> 1656[label="",style="solid", color="black", weight=3];
1485[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu71))) (primCmpNat Zero (Succ yu1020) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1485 -> 1500[label="",style="solid", color="black", weight=3];
1486[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu71))) (EQ == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1486 -> 1501[label="",style="solid", color="black", weight=3];
6032 -> 1618[label="",style="dashed", color="red", weight=0];
6032[label="primMulNat yu485 (Succ Zero)",fontsize=16,color="magenta"];6032 -> 6043[label="",style="dashed", color="magenta", weight=3];
6031[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (primCmpInt (Pos Zero) (Neg yu491) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6341[label="yu491/Succ yu4910",fontsize=10,color="white",style="solid",shape="box"];6031 -> 6341[label="",style="solid", color="burlywood", weight=9];
6341 -> 6044[label="",style="solid", color="burlywood", weight=3];
6342[label="yu491/Zero",fontsize=10,color="white",style="solid",shape="box"];6031 -> 6342[label="",style="solid", color="burlywood", weight=9];
6342 -> 6045[label="",style="solid", color="burlywood", weight=3];
1638[label="Succ yu3100",fontsize=16,color="green",shape="box"];1639[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu78))) (GT == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1639 -> 1657[label="",style="solid", color="black", weight=3];
1640[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu78))) (EQ == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1640 -> 1658[label="",style="solid", color="black", weight=3];
3627[label="Succ yu243",fontsize=16,color="green",shape="box"];3628 -> 3649[label="",style="dashed", color="red", weight=0];
3628[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Pos Zero) (Pos (primMulNat yu354 (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];3628 -> 3650[label="",style="dashed", color="magenta", weight=3];
3629[label="Succ yu243",fontsize=16,color="green",shape="box"];3630 -> 3651[label="",style="dashed", color="red", weight=0];
3630[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Neg Zero) (Pos (primMulNat yu355 (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];3630 -> 3652[label="",style="dashed", color="magenta", weight=3];
1878[label="Succ yu3100",fontsize=16,color="green",shape="box"];1879[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu87))) (primCmpNat Zero (Succ yu1520) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1879 -> 1891[label="",style="solid", color="black", weight=3];
1880[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu87))) (EQ == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1880 -> 1892[label="",style="solid", color="black", weight=3];
6038 -> 1618[label="",style="dashed", color="red", weight=0];
6038[label="primMulNat yu486 (Succ Zero)",fontsize=16,color="magenta"];6038 -> 6046[label="",style="dashed", color="magenta", weight=3];
6037[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpInt (Neg Zero) (Neg yu492) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6346[label="yu492/Succ yu4920",fontsize=10,color="white",style="solid",shape="box"];6037 -> 6346[label="",style="solid", color="burlywood", weight=9];
6346 -> 6047[label="",style="solid", color="burlywood", weight=3];
6347[label="yu492/Zero",fontsize=10,color="white",style="solid",shape="box"];6037 -> 6347[label="",style="solid", color="burlywood", weight=9];
6347 -> 6048[label="",style="solid", color="burlywood", weight=3];
2072[label="Succ yu3100",fontsize=16,color="green",shape="box"];2073[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu94))) (primCmpNat (Succ yu1960) Zero == GT)\n  Integral a",fontsize=16,color="black",shape="box"];2073 -> 2084[label="",style="solid", color="black", weight=3];
2074[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu94))) (EQ == GT)\n  Integral a",fontsize=16,color="black",shape="box"];2074 -> 2085[label="",style="solid", color="black", weight=3];
5731 -> 5749[label="",style="dashed", color="red", weight=0];
5731[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Pos Zero) (primMulInt (Pos (primMulNat (Succ yu320) (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];5731 -> 5750[label="",style="dashed", color="magenta", weight=3];
4911[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (primCmpInt (Neg Zero) (primMulInt (primMulInt (Pos (Succ yu418)) (Pos (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];4911 -> 4951[label="",style="solid", color="black", weight=3];
3899 -> 3948[label="",style="dashed", color="red", weight=0];
3899[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Pos Zero) (primMulInt (Pos (primMulNat (Succ yu206) (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];3899 -> 3949[label="",style="dashed", color="magenta", weight=3];
6039 -> 5998[label="",style="dashed", color="red", weight=0];
6039[label="primDivNatS (primMinusNatS yu4880 yu4890) (Succ yu490)",fontsize=16,color="magenta"];6039 -> 6100[label="",style="dashed", color="magenta", weight=3];
6039 -> 6101[label="",style="dashed", color="magenta", weight=3];
6040 -> 5676[label="",style="dashed", color="red", weight=0];
6040[label="primDivNatS (Succ yu4880) (Succ yu490)",fontsize=16,color="magenta"];6040 -> 6102[label="",style="dashed", color="magenta", weight=3];
6040 -> 6103[label="",style="dashed", color="magenta", weight=3];
6041 -> 2540[label="",style="dashed", color="red", weight=0];
6041[label="primDivNatS Zero (Succ yu490)",fontsize=16,color="magenta"];6041 -> 6104[label="",style="dashed", color="magenta", weight=3];
6042 -> 2540[label="",style="dashed", color="red", weight=0];
6042[label="primDivNatS Zero (Succ yu490)",fontsize=16,color="magenta"];6042 -> 6105[label="",style="dashed", color="magenta", weight=3];
1655 -> 1668[label="",style="dashed", color="red", weight=0];
1655[label="primPlusNat (primMulNat yu1130 (Succ Zero)) (Succ Zero)",fontsize=16,color="magenta"];1655 -> 1669[label="",style="dashed", color="magenta", weight=3];
1656[label="Zero",fontsize=16,color="green",shape="box"];1500[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu71))) (LT == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1500 -> 1516[label="",style="solid", color="black", weight=3];
1501[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu71))) False\n  Integral a",fontsize=16,color="black",shape="triangle"];1501 -> 1517[label="",style="solid", color="black", weight=3];
6043[label="yu485",fontsize=16,color="green",shape="box"];6044[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (primCmpInt (Pos Zero) (Neg (Succ yu4910)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];6044 -> 6106[label="",style="solid", color="black", weight=3];
6045[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (primCmpInt (Pos Zero) (Neg Zero) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];6045 -> 6107[label="",style="solid", color="black", weight=3];
1657[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu78))) True\n  Integral a",fontsize=16,color="black",shape="box"];1657 -> 1682[label="",style="solid", color="black", weight=3];
1658[label="ceilingCeiling0 (Float (Pos Zero) (Neg (Succ yu78))) False\n  Integral a",fontsize=16,color="black",shape="box"];1658 -> 1683[label="",style="solid", color="black", weight=3];
3650 -> 1618[label="",style="dashed", color="red", weight=0];
3650[label="primMulNat yu354 (Succ Zero)",fontsize=16,color="magenta"];3650 -> 3674[label="",style="dashed", color="magenta", weight=3];
3649[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Pos Zero) (Pos yu359) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6356[label="yu359/Succ yu3590",fontsize=10,color="white",style="solid",shape="box"];3649 -> 6356[label="",style="solid", color="burlywood", weight=9];
6356 -> 3675[label="",style="solid", color="burlywood", weight=3];
6357[label="yu359/Zero",fontsize=10,color="white",style="solid",shape="box"];3649 -> 6357[label="",style="solid", color="burlywood", weight=9];
6357 -> 3676[label="",style="solid", color="burlywood", weight=3];
3652 -> 1618[label="",style="dashed", color="red", weight=0];
3652[label="primMulNat yu355 (Succ Zero)",fontsize=16,color="magenta"];3652 -> 3677[label="",style="dashed", color="magenta", weight=3];
3651[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Neg Zero) (Pos yu360) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6359[label="yu360/Succ yu3600",fontsize=10,color="white",style="solid",shape="box"];3651 -> 6359[label="",style="solid", color="burlywood", weight=9];
6359 -> 3678[label="",style="solid", color="burlywood", weight=3];
6360[label="yu360/Zero",fontsize=10,color="white",style="solid",shape="box"];3651 -> 6360[label="",style="solid", color="burlywood", weight=9];
6360 -> 3679[label="",style="solid", color="burlywood", weight=3];
1891[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu87))) (LT == GT)\n  Integral a",fontsize=16,color="black",shape="box"];1891 -> 1905[label="",style="solid", color="black", weight=3];
1892[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu87))) False\n  Integral a",fontsize=16,color="black",shape="triangle"];1892 -> 1906[label="",style="solid", color="black", weight=3];
6046[label="yu486",fontsize=16,color="green",shape="box"];6047[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpInt (Neg Zero) (Neg (Succ yu4920)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];6047 -> 6108[label="",style="solid", color="black", weight=3];
6048[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpInt (Neg Zero) (Neg Zero) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];6048 -> 6109[label="",style="solid", color="black", weight=3];
2084[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu94))) (GT == GT)\n  Integral a",fontsize=16,color="black",shape="box"];2084 -> 2100[label="",style="solid", color="black", weight=3];
2085[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu94))) False\n  Integral a",fontsize=16,color="black",shape="box"];2085 -> 2101[label="",style="solid", color="black", weight=3];
5750 -> 1618[label="",style="dashed", color="red", weight=0];
5750[label="primMulNat (Succ yu320) (Succ Zero)",fontsize=16,color="magenta"];5750 -> 5751[label="",style="dashed", color="magenta", weight=3];
5749[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Pos Zero) (primMulInt (Pos yu460) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5749 -> 5752[label="",style="solid", color="black", weight=3];
4951 -> 4978[label="",style="dashed", color="red", weight=0];
4951[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (primCmpInt (Neg Zero) (primMulInt (Pos (primMulNat (Succ yu418) (Succ Zero))) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];4951 -> 4979[label="",style="dashed", color="magenta", weight=3];
3949 -> 1618[label="",style="dashed", color="red", weight=0];
3949[label="primMulNat (Succ yu206) (Succ Zero)",fontsize=16,color="magenta"];3949 -> 3952[label="",style="dashed", color="magenta", weight=3];
3948[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Pos Zero) (primMulInt (Pos yu371) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3948 -> 3953[label="",style="solid", color="black", weight=3];
6100[label="yu4890",fontsize=16,color="green",shape="box"];6101[label="yu4880",fontsize=16,color="green",shape="box"];6102[label="yu4880",fontsize=16,color="green",shape="box"];6103[label="yu490",fontsize=16,color="green",shape="box"];5676[label="primDivNatS (Succ yu451) (Succ yu452)",fontsize=16,color="black",shape="triangle"];5676 -> 5690[label="",style="solid", color="black", weight=3];
6104[label="yu490",fontsize=16,color="green",shape="box"];2540[label="primDivNatS Zero (Succ yu71)",fontsize=16,color="black",shape="triangle"];2540 -> 2831[label="",style="solid", color="black", weight=3];
6105[label="yu490",fontsize=16,color="green",shape="box"];1669 -> 1618[label="",style="dashed", color="red", weight=0];
1669[label="primMulNat yu1130 (Succ Zero)",fontsize=16,color="magenta"];1669 -> 1684[label="",style="dashed", color="magenta", weight=3];
1668[label="primPlusNat yu118 (Succ Zero)",fontsize=16,color="burlywood",shape="triangle"];6365[label="yu118/Succ yu1180",fontsize=10,color="white",style="solid",shape="box"];1668 -> 6365[label="",style="solid", color="burlywood", weight=9];
6365 -> 1685[label="",style="solid", color="burlywood", weight=3];
6366[label="yu118/Zero",fontsize=10,color="white",style="solid",shape="box"];1668 -> 6366[label="",style="solid", color="burlywood", weight=9];
6366 -> 1686[label="",style="solid", color="burlywood", weight=3];
1516 -> 1501[label="",style="dashed", color="red", weight=0];
1516[label="ceilingCeiling0 (Float (Pos Zero) (Pos (Succ yu71))) False\n  Integral a",fontsize=16,color="magenta"];1517[label="ceilingN (Float (Pos Zero) (Pos (Succ yu71)))\n  Integral a",fontsize=16,color="black",shape="box"];1517 -> 1531[label="",style="solid", color="black", weight=3];
6106[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (GT == GT)\n  Integral a",fontsize=16,color="black",shape="box"];6106 -> 6114[label="",style="solid", color="black", weight=3];
6107[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (EQ == GT)\n  Integral a",fontsize=16,color="black",shape="box"];6107 -> 6115[label="",style="solid", color="black", weight=3];
1682[label="ceilingN (Float (Pos Zero) (Neg (Succ yu78))) + fromInt (Pos (Succ Zero))\n  Integral a",fontsize=16,color="blue",shape="box"];6368[label="+ :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];1682 -> 6368[label="",style="solid", color="blue", weight=9];
6368 -> 1701[label="",style="solid", color="blue", weight=3];
6369[label="+ :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1682 -> 6369[label="",style="solid", color="blue", weight=9];
6369 -> 1702[label="",style="solid", color="blue", weight=3];
1683[label="ceilingN (Float (Pos Zero) (Neg (Succ yu78)))\n  Integral a",fontsize=16,color="black",shape="triangle"];1683 -> 1703[label="",style="solid", color="black", weight=3];
3674[label="yu354",fontsize=16,color="green",shape="box"];3675[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Pos Zero) (Pos (Succ yu3590)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3675 -> 3732[label="",style="solid", color="black", weight=3];
3676[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Pos Zero) (Pos Zero) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3676 -> 3733[label="",style="solid", color="black", weight=3];
3677[label="yu355",fontsize=16,color="green",shape="box"];3678[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Neg Zero) (Pos (Succ yu3600)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3678 -> 3734[label="",style="solid", color="black", weight=3];
3679[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpInt (Neg Zero) (Pos Zero) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3679 -> 3735[label="",style="solid", color="black", weight=3];
1905 -> 1892[label="",style="dashed", color="red", weight=0];
1905[label="ceilingCeiling0 (Float (Neg Zero) (Pos (Succ yu87))) False\n  Integral a",fontsize=16,color="magenta"];1906[label="ceilingN (Float (Neg Zero) (Pos (Succ yu87)))\n  Integral a",fontsize=16,color="black",shape="box"];1906 -> 1918[label="",style="solid", color="black", weight=3];
6108[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (primCmpNat (Succ yu4920) Zero == GT)\n  Integral a",fontsize=16,color="black",shape="box"];6108 -> 6116[label="",style="solid", color="black", weight=3];
6109[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (EQ == GT)\n  Integral a",fontsize=16,color="black",shape="box"];6109 -> 6117[label="",style="solid", color="black", weight=3];
2100[label="ceilingCeiling0 (Float (Neg Zero) (Neg (Succ yu94))) True\n  Integral a",fontsize=16,color="black",shape="box"];2100 -> 2109[label="",style="solid", color="black", weight=3];
2101[label="ceilingN (Float (Neg Zero) (Neg (Succ yu94)))\n  Integral a",fontsize=16,color="black",shape="triangle"];2101 -> 2110[label="",style="solid", color="black", weight=3];
5751[label="Succ yu320",fontsize=16,color="green",shape="box"];5752 -> 5757[label="",style="dashed", color="red", weight=0];
5752[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Pos Zero) (Pos (primMulNat yu460 (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];5752 -> 5758[label="",style="dashed", color="magenta", weight=3];
4979 -> 1618[label="",style="dashed", color="red", weight=0];
4979[label="primMulNat (Succ yu418) (Succ Zero)",fontsize=16,color="magenta"];4979 -> 4982[label="",style="dashed", color="magenta", weight=3];
4978[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (primCmpInt (Neg Zero) (primMulInt (Pos yu428) (Pos (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];4978 -> 4983[label="",style="solid", color="black", weight=3];
3952[label="Succ yu206",fontsize=16,color="green",shape="box"];3953 -> 3973[label="",style="dashed", color="red", weight=0];
3953[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Pos Zero) (Pos (primMulNat yu371 (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];3953 -> 3974[label="",style="dashed", color="magenta", weight=3];
5690 -> 4382[label="",style="dashed", color="red", weight=0];
5690[label="primDivNatS0 yu451 yu452 (primGEqNatS yu451 yu452)",fontsize=16,color="magenta"];5690 -> 5702[label="",style="dashed", color="magenta", weight=3];
5690 -> 5703[label="",style="dashed", color="magenta", weight=3];
2831[label="Zero",fontsize=16,color="green",shape="box"];1684[label="yu1130",fontsize=16,color="green",shape="box"];1685[label="primPlusNat (Succ yu1180) (Succ Zero)",fontsize=16,color="black",shape="box"];1685 -> 1704[label="",style="solid", color="black", weight=3];
1686[label="primPlusNat Zero (Succ Zero)",fontsize=16,color="black",shape="box"];1686 -> 1705[label="",style="solid", color="black", weight=3];
1531[label="ceilingN0 (Float (Pos Zero) (Pos (Succ yu71))) (ceilingVu8 (Float (Pos Zero) (Pos (Succ yu71))))\n  Integral a",fontsize=16,color="black",shape="box"];1531 -> 1547[label="",style="solid", color="black", weight=3];
6114[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) True\n  Integral a",fontsize=16,color="black",shape="box"];6114 -> 6122[label="",style="solid", color="black", weight=3];
6115[label="ceilingCeiling0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) False\n  Integral a",fontsize=16,color="black",shape="box"];6115 -> 6123[label="",style="solid", color="black", weight=3];
1701[label="ceilingN (Float (Pos Zero) (Neg (Succ yu78))) + fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1701 -> 2139[label="",style="solid", color="black", weight=3];
1702[label="ceilingN (Float (Pos Zero) (Neg (Succ yu78))) + fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1702 -> 2140[label="",style="solid", color="black", weight=3];
1703[label="ceilingN0 (Float (Pos Zero) (Neg (Succ yu78))) (ceilingVu8 (Float (Pos Zero) (Neg (Succ yu78))))\n  Integral a",fontsize=16,color="black",shape="box"];1703 -> 1720[label="",style="solid", color="black", weight=3];
3732[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (primCmpNat Zero (Succ yu3590) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3732 -> 3766[label="",style="solid", color="black", weight=3];
3733[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (EQ == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3733 -> 3767[label="",style="solid", color="black", weight=3];
3734[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (LT == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];3734 -> 3768[label="",style="solid", color="black", weight=3];
3735 -> 3733[label="",style="dashed", color="red", weight=0];
3735[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (EQ == GT)\n  Integral a",fontsize=16,color="magenta"];1918[label="ceilingN0 (Float (Neg Zero) (Pos (Succ yu87))) (ceilingVu8 (Float (Neg Zero) (Pos (Succ yu87))))\n  Integral a",fontsize=16,color="black",shape="box"];1918 -> 1927[label="",style="solid", color="black", weight=3];
6116[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (GT == GT)\n  Integral a",fontsize=16,color="black",shape="box"];6116 -> 6124[label="",style="solid", color="black", weight=3];
6117[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) False\n  Integral a",fontsize=16,color="black",shape="box"];6117 -> 6125[label="",style="solid", color="black", weight=3];
2109[label="ceilingN (Float (Neg Zero) (Neg (Succ yu94))) + fromInt (Pos (Succ Zero))\n  Integral a",fontsize=16,color="blue",shape="box"];6376[label="+ :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];2109 -> 6376[label="",style="solid", color="blue", weight=9];
6376 -> 2141[label="",style="solid", color="blue", weight=3];
6377[label="+ :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];2109 -> 6377[label="",style="solid", color="blue", weight=9];
6377 -> 2142[label="",style="solid", color="blue", weight=3];
2110[label="ceilingN0 (Float (Neg Zero) (Neg (Succ yu94))) (ceilingVu8 (Float (Neg Zero) (Neg (Succ yu94))))\n  Integral a",fontsize=16,color="black",shape="box"];2110 -> 2128[label="",style="solid", color="black", weight=3];
5758 -> 1618[label="",style="dashed", color="red", weight=0];
5758[label="primMulNat yu460 (Succ Zero)",fontsize=16,color="magenta"];5758 -> 5759[label="",style="dashed", color="magenta", weight=3];
5757[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Pos Zero) (Pos yu463) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6379[label="yu463/Succ yu4630",fontsize=10,color="white",style="solid",shape="box"];5757 -> 6379[label="",style="solid", color="burlywood", weight=9];
6379 -> 5760[label="",style="solid", color="burlywood", weight=3];
6380[label="yu463/Zero",fontsize=10,color="white",style="solid",shape="box"];5757 -> 6380[label="",style="solid", color="burlywood", weight=9];
6380 -> 5761[label="",style="solid", color="burlywood", weight=3];
4982[label="Succ yu418",fontsize=16,color="green",shape="box"];4983 -> 4998[label="",style="dashed", color="red", weight=0];
4983[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (primCmpInt (Neg Zero) (Pos (primMulNat yu428 (Succ Zero))) == GT)\n  Integral a",fontsize=16,color="magenta"];4983 -> 4999[label="",style="dashed", color="magenta", weight=3];
3974 -> 1618[label="",style="dashed", color="red", weight=0];
3974[label="primMulNat yu371 (Succ Zero)",fontsize=16,color="magenta"];3974 -> 3977[label="",style="dashed", color="magenta", weight=3];
3973[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Pos Zero) (Pos yu375) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6383[label="yu375/Succ yu3750",fontsize=10,color="white",style="solid",shape="box"];3973 -> 6383[label="",style="solid", color="burlywood", weight=9];
6383 -> 3978[label="",style="solid", color="burlywood", weight=3];
6384[label="yu375/Zero",fontsize=10,color="white",style="solid",shape="box"];3973 -> 6384[label="",style="solid", color="burlywood", weight=9];
6384 -> 3979[label="",style="solid", color="burlywood", weight=3];
5702[label="yu452",fontsize=16,color="green",shape="box"];5703[label="yu451",fontsize=16,color="green",shape="box"];1704[label="Succ (Succ (primPlusNat yu1180 Zero))",fontsize=16,color="green",shape="box"];1704 -> 1721[label="",style="dashed", color="green", weight=3];
1705[label="Succ Zero",fontsize=16,color="green",shape="box"];1547[label="ceilingN0 (Float (Pos Zero) (Pos (Succ yu71))) (properFraction (Float (Pos Zero) (Pos (Succ yu71))))\n  Integral a",fontsize=16,color="black",shape="box"];1547 -> 1560[label="",style="solid", color="black", weight=3];
6122[label="ceilingN (Float (Pos (Succ yu470)) (Neg (Succ yu471))) + fromInt (Pos (Succ Zero))\n  Integral a",fontsize=16,color="blue",shape="box"];6385[label="+ :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];6122 -> 6385[label="",style="solid", color="blue", weight=9];
6385 -> 6133[label="",style="solid", color="blue", weight=3];
6386[label="+ :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];6122 -> 6386[label="",style="solid", color="blue", weight=9];
6386 -> 6134[label="",style="solid", color="blue", weight=3];
6123[label="ceilingN (Float (Pos (Succ yu470)) (Neg (Succ yu471)))\n  Integral a",fontsize=16,color="black",shape="triangle"];6123 -> 6135[label="",style="solid", color="black", weight=3];
2139[label="error []",fontsize=16,color="red",shape="box"];2140 -> 2152[label="",style="dashed", color="red", weight=0];
2140[label="primPlusInt (ceilingN (Float (Pos Zero) (Neg (Succ yu78)))) (fromInt (Pos (Succ Zero)))",fontsize=16,color="magenta"];2140 -> 2153[label="",style="dashed", color="magenta", weight=3];
1720[label="ceilingN0 (Float (Pos Zero) (Neg (Succ yu78))) (properFraction (Float (Pos Zero) (Neg (Succ yu78))))\n  Integral a",fontsize=16,color="black",shape="box"];1720 -> 1729[label="",style="solid", color="black", weight=3];
3766 -> 3734[label="",style="dashed", color="red", weight=0];
3766[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (LT == GT)\n  Integral a",fontsize=16,color="magenta"];3767[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) False\n  Integral a",fontsize=16,color="black",shape="triangle"];3767 -> 3802[label="",style="solid", color="black", weight=3];
3768 -> 3767[label="",style="dashed", color="red", weight=0];
3768[label="ceilingCeiling0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) False\n  Integral a",fontsize=16,color="magenta"];1927[label="ceilingN0 (Float (Neg Zero) (Pos (Succ yu87))) (properFraction (Float (Neg Zero) (Pos (Succ yu87))))\n  Integral a",fontsize=16,color="black",shape="box"];1927 -> 1933[label="",style="solid", color="black", weight=3];
6124[label="ceilingCeiling0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) True\n  Integral a",fontsize=16,color="black",shape="box"];6124 -> 6136[label="",style="solid", color="black", weight=3];
6125[label="ceilingN (Float (Neg (Succ yu476)) (Neg (Succ yu477)))\n  Integral a",fontsize=16,color="black",shape="triangle"];6125 -> 6137[label="",style="solid", color="black", weight=3];
2141[label="ceilingN (Float (Neg Zero) (Neg (Succ yu94))) + fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];2141 -> 2720[label="",style="solid", color="black", weight=3];
2142[label="ceilingN (Float (Neg Zero) (Neg (Succ yu94))) + fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];2142 -> 2721[label="",style="solid", color="black", weight=3];
2128[label="ceilingN0 (Float (Neg Zero) (Neg (Succ yu94))) (properFraction (Float (Neg Zero) (Neg (Succ yu94))))\n  Integral a",fontsize=16,color="black",shape="box"];2128 -> 2143[label="",style="solid", color="black", weight=3];
5759[label="yu460",fontsize=16,color="green",shape="box"];5760[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Pos Zero) (Pos (Succ yu4630)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5760 -> 5768[label="",style="solid", color="black", weight=3];
5761[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpInt (Pos Zero) (Pos Zero) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5761 -> 5769[label="",style="solid", color="black", weight=3];
4999 -> 1618[label="",style="dashed", color="red", weight=0];
4999[label="primMulNat yu428 (Succ Zero)",fontsize=16,color="magenta"];4999 -> 5013[label="",style="dashed", color="magenta", weight=3];
4998[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (primCmpInt (Neg Zero) (Pos yu432) == GT)\n  Integral a",fontsize=16,color="burlywood",shape="triangle"];6391[label="yu432/Succ yu4320",fontsize=10,color="white",style="solid",shape="box"];4998 -> 6391[label="",style="solid", color="burlywood", weight=9];
6391 -> 5014[label="",style="solid", color="burlywood", weight=3];
6392[label="yu432/Zero",fontsize=10,color="white",style="solid",shape="box"];4998 -> 6392[label="",style="solid", color="burlywood", weight=9];
6392 -> 5015[label="",style="solid", color="burlywood", weight=3];
3977[label="yu371",fontsize=16,color="green",shape="box"];3978[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Pos Zero) (Pos (Succ yu3750)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3978 -> 4067[label="",style="solid", color="black", weight=3];
3979[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpInt (Pos Zero) (Pos Zero) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];3979 -> 4068[label="",style="solid", color="black", weight=3];
1721[label="primPlusNat yu1180 Zero",fontsize=16,color="burlywood",shape="box"];6393[label="yu1180/Succ yu11800",fontsize=10,color="white",style="solid",shape="box"];1721 -> 6393[label="",style="solid", color="burlywood", weight=9];
6393 -> 1730[label="",style="solid", color="burlywood", weight=3];
6394[label="yu1180/Zero",fontsize=10,color="white",style="solid",shape="box"];1721 -> 6394[label="",style="solid", color="burlywood", weight=9];
6394 -> 1731[label="",style="solid", color="burlywood", weight=3];
1560[label="ceilingN0 (Float (Pos Zero) (Pos (Succ yu71))) (floatProperFractionFloat (Float (Pos Zero) (Pos (Succ yu71))))\n  Integral a",fontsize=16,color="black",shape="box"];1560 -> 1641[label="",style="solid", color="black", weight=3];
6133[label="ceilingN (Float (Pos (Succ yu470)) (Neg (Succ yu471))) + fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];6133 -> 6159[label="",style="solid", color="black", weight=3];
6134[label="ceilingN (Float (Pos (Succ yu470)) (Neg (Succ yu471))) + fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];6134 -> 6158[label="",style="solid", color="black", weight=3];
6135[label="ceilingN0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (ceilingVu8 (Float (Pos (Succ yu470)) (Neg (Succ yu471))))\n  Integral a",fontsize=16,color="black",shape="box"];6135 -> 6142[label="",style="solid", color="black", weight=3];
2153 -> 1683[label="",style="dashed", color="red", weight=0];
2153[label="ceilingN (Float (Pos Zero) (Neg (Succ yu78)))",fontsize=16,color="magenta"];2152[label="primPlusInt yu220 (fromInt (Pos (Succ Zero)))",fontsize=16,color="burlywood",shape="triangle"];6396[label="yu220/Pos yu2200",fontsize=10,color="white",style="solid",shape="box"];2152 -> 6396[label="",style="solid", color="burlywood", weight=9];
6396 -> 2158[label="",style="solid", color="burlywood", weight=3];
6397[label="yu220/Neg yu2200",fontsize=10,color="white",style="solid",shape="box"];2152 -> 6397[label="",style="solid", color="burlywood", weight=9];
6397 -> 2159[label="",style="solid", color="burlywood", weight=3];
1729[label="ceilingN0 (Float (Pos Zero) (Neg (Succ yu78))) (floatProperFractionFloat (Float (Pos Zero) (Neg (Succ yu78))))\n  Integral a",fontsize=16,color="black",shape="box"];1729 -> 1742[label="",style="solid", color="black", weight=3];
3802[label="ceilingN (Float (Neg (Succ yu242)) (Pos (Succ yu243)))\n  Integral a",fontsize=16,color="black",shape="box"];3802 -> 3850[label="",style="solid", color="black", weight=3];
1933[label="ceilingN0 (Float (Neg Zero) (Pos (Succ yu87))) (floatProperFractionFloat (Float (Neg Zero) (Pos (Succ yu87))))\n  Integral a",fontsize=16,color="black",shape="box"];1933 -> 1943[label="",style="solid", color="black", weight=3];
6136[label="ceilingN (Float (Neg (Succ yu476)) (Neg (Succ yu477))) + fromInt (Pos (Succ Zero))\n  Integral a",fontsize=16,color="blue",shape="box"];6398[label="+ :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];6136 -> 6398[label="",style="solid", color="blue", weight=9];
6398 -> 6156[label="",style="solid", color="blue", weight=3];
6399[label="+ :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];6136 -> 6399[label="",style="solid", color="blue", weight=9];
6399 -> 6157[label="",style="solid", color="blue", weight=3];
6137[label="ceilingN0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (ceilingVu8 (Float (Neg (Succ yu476)) (Neg (Succ yu477))))\n  Integral a",fontsize=16,color="black",shape="box"];6137 -> 6149[label="",style="solid", color="black", weight=3];
2720[label="error []",fontsize=16,color="red",shape="box"];2721 -> 2152[label="",style="dashed", color="red", weight=0];
2721[label="primPlusInt (ceilingN (Float (Neg Zero) (Neg (Succ yu94)))) (fromInt (Pos (Succ Zero)))",fontsize=16,color="magenta"];2721 -> 2746[label="",style="dashed", color="magenta", weight=3];
2143[label="ceilingN0 (Float (Neg Zero) (Neg (Succ yu94))) (floatProperFractionFloat (Float (Neg Zero) (Neg (Succ yu94))))\n  Integral a",fontsize=16,color="black",shape="box"];2143 -> 2162[label="",style="solid", color="black", weight=3];
5768 -> 4350[label="",style="dashed", color="red", weight=0];
5768[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (primCmpNat Zero (Succ yu4630) == GT)\n  Integral a",fontsize=16,color="magenta"];5768 -> 5773[label="",style="dashed", color="magenta", weight=3];
5768 -> 5774[label="",style="dashed", color="magenta", weight=3];
5768 -> 5775[label="",style="dashed", color="magenta", weight=3];
5769 -> 5030[label="",style="dashed", color="red", weight=0];
5769[label="ceilingCeiling0 (Float (Pos (Succ (Succ yu3190))) (Pos (Succ yu320))) (EQ == GT)\n  Integral a",fontsize=16,color="magenta"];5769 -> 5776[label="",style="dashed", color="magenta", weight=3];
5769 -> 5777[label="",style="dashed", color="magenta", weight=3];
5013[label="yu428",fontsize=16,color="green",shape="box"];5014[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (primCmpInt (Neg Zero) (Pos (Succ yu4320)) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5014 -> 5029[label="",style="solid", color="black", weight=3];
5015[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (primCmpInt (Neg Zero) (Pos Zero) == GT)\n  Integral a",fontsize=16,color="black",shape="box"];5015 -> 5030[label="",style="solid", color="black", weight=3];
4067 -> 4350[label="",style="dashed", color="red", weight=0];
4067[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (primCmpNat Zero (Succ yu3750) == GT)\n  Integral a",fontsize=16,color="magenta"];4067 -> 4351[label="",style="dashed", color="magenta", weight=3];
4067 -> 4352[label="",style="dashed", color="magenta", weight=3];
4067 -> 4353[label="",style="dashed", color="magenta", weight=3];
4068[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (EQ == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];4068 -> 4104[label="",style="solid", color="black", weight=3];
1730[label="primPlusNat (Succ yu11800) Zero",fontsize=16,color="black",shape="box"];1730 -> 1743[label="",style="solid", color="black", weight=3];
1731[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];1731 -> 1744[label="",style="solid", color="black", weight=3];
1641[label="ceilingN0 (Float (Pos Zero) (Pos (Succ yu71))) (fromInt (Pos Zero `quot` Pos (Succ yu71)),Float (Pos Zero) (Pos (Succ yu71)) - fromInt (Pos Zero `quot` Pos (Succ yu71)))\n  Integral a",fontsize=16,color="black",shape="box"];1641 -> 1659[label="",style="solid", color="black", weight=3];
6159[label="error []",fontsize=16,color="red",shape="box"];6158 -> 2152[label="",style="dashed", color="red", weight=0];
6158[label="primPlusInt (ceilingN (Float (Pos (Succ yu470)) (Neg (Succ yu471)))) (fromInt (Pos (Succ Zero)))",fontsize=16,color="magenta"];6158 -> 6167[label="",style="dashed", color="magenta", weight=3];
6142[label="ceilingN0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (properFraction (Float (Pos (Succ yu470)) (Neg (Succ yu471))))\n  Integral a",fontsize=16,color="black",shape="box"];6142 -> 6152[label="",style="solid", color="black", weight=3];
2158[label="primPlusInt (Pos yu2200) (fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];2158 -> 2176[label="",style="solid", color="black", weight=3];
2159[label="primPlusInt (Neg yu2200) (fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];2159 -> 2177[label="",style="solid", color="black", weight=3];
1742[label="ceilingN0 (Float (Pos Zero) (Neg (Succ yu78))) (fromInt (Pos Zero `quot` Neg (Succ yu78)),Float (Pos Zero) (Neg (Succ yu78)) - fromInt (Pos Zero `quot` Neg (Succ yu78)))\n  Integral a",fontsize=16,color="black",shape="box"];1742 -> 1749[label="",style="solid", color="black", weight=3];
3850[label="ceilingN0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (ceilingVu8 (Float (Neg (Succ yu242)) (Pos (Succ yu243))))\n  Integral a",fontsize=16,color="black",shape="box"];3850 -> 3884[label="",style="solid", color="black", weight=3];
1943[label="ceilingN0 (Float (Neg Zero) (Pos (Succ yu87))) (fromInt (Neg Zero `quot` Pos (Succ yu87)),Float (Neg Zero) (Pos (Succ yu87)) - fromInt (Neg Zero `quot` Pos (Succ yu87)))\n  Integral a",fontsize=16,color="black",shape="box"];1943 -> 1952[label="",style="solid", color="black", weight=3];
6156 -> 6138[label="",style="dashed", color="red", weight=0];
6156[label="ceilingN (Float (Neg (Succ yu476)) (Neg (Succ yu477))) + fromInt (Pos (Succ Zero))",fontsize=16,color="magenta"];6156 -> 6165[label="",style="dashed", color="magenta", weight=3];
6157 -> 6140[label="",style="dashed", color="red", weight=0];
6157[label="ceilingN (Float (Neg (Succ yu476)) (Neg (Succ yu477))) + fromInt (Pos (Succ Zero))",fontsize=16,color="magenta"];6157 -> 6166[label="",style="dashed", color="magenta", weight=3];
6149[label="ceilingN0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (properFraction (Float (Neg (Succ yu476)) (Neg (Succ yu477))))\n  Integral a",fontsize=16,color="black",shape="box"];6149 -> 6153[label="",style="solid", color="black", weight=3];
2746 -> 2101[label="",style="dashed", color="red", weight=0];
2746[label="ceilingN (Float (Neg Zero) (Neg (Succ yu94)))",fontsize=16,color="magenta"];2162[label="ceilingN0 (Float (Neg Zero) (Neg (Succ yu94))) (fromInt (Neg Zero `quot` Neg (Succ yu94)),Float (Neg Zero) (Neg (Succ yu94)) - fromInt (Neg Zero `quot` Neg (Succ yu94)))\n  Integral a",fontsize=16,color="black",shape="box"];2162 -> 2179[label="",style="solid", color="black", weight=3];
5773[label="Succ yu3190",fontsize=16,color="green",shape="box"];5774[label="yu4630",fontsize=16,color="green",shape="box"];5775[label="yu320",fontsize=16,color="green",shape="box"];4350[label="ceilingCeiling0 (Float (Pos (Succ yu403)) (Pos (Succ yu404))) (primCmpNat Zero (Succ yu405) == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];4350 -> 4375[label="",style="solid", color="black", weight=3];
5776[label="yu320",fontsize=16,color="green",shape="box"];5777[label="Succ yu3190",fontsize=16,color="green",shape="box"];5030[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (EQ == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];5030 -> 5143[label="",style="solid", color="black", weight=3];
5029 -> 4375[label="",style="dashed", color="red", weight=0];
5029[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) (LT == GT)\n  Integral a",fontsize=16,color="magenta"];5029 -> 5141[label="",style="dashed", color="magenta", weight=3];
5029 -> 5142[label="",style="dashed", color="magenta", weight=3];
4351[label="Zero",fontsize=16,color="green",shape="box"];4352[label="yu3750",fontsize=16,color="green",shape="box"];4353[label="yu206",fontsize=16,color="green",shape="box"];4104[label="ceilingCeiling0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) False\n  Integral a",fontsize=16,color="black",shape="triangle"];4104 -> 4157[label="",style="solid", color="black", weight=3];
1743[label="Succ yu11800",fontsize=16,color="green",shape="box"];1744[label="Zero",fontsize=16,color="green",shape="box"];1659[label="fromInt (Pos Zero `quot` Pos (Succ yu71))\n  Integral a",fontsize=16,color="blue",shape="box"];6409[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];1659 -> 6409[label="",style="solid", color="blue", weight=9];
6409 -> 1687[label="",style="solid", color="blue", weight=3];
6410[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1659 -> 6410[label="",style="solid", color="blue", weight=9];
6410 -> 1688[label="",style="solid", color="blue", weight=3];
6167 -> 6123[label="",style="dashed", color="red", weight=0];
6167[label="ceilingN (Float (Pos (Succ yu470)) (Neg (Succ yu471)))",fontsize=16,color="magenta"];6152[label="ceilingN0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (floatProperFractionFloat (Float (Pos (Succ yu470)) (Neg (Succ yu471))))\n  Integral a",fontsize=16,color="black",shape="box"];6152 -> 6162[label="",style="solid", color="black", weight=3];
2176[label="primPlusInt (Pos yu2200) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];2176 -> 2198[label="",style="solid", color="black", weight=3];
2177[label="primPlusInt (Neg yu2200) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];2177 -> 2199[label="",style="solid", color="black", weight=3];
1749[label="fromInt (Pos Zero `quot` Neg (Succ yu78))\n  Integral a",fontsize=16,color="blue",shape="box"];6412[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];1749 -> 6412[label="",style="solid", color="blue", weight=9];
6412 -> 1754[label="",style="solid", color="blue", weight=3];
6413[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1749 -> 6413[label="",style="solid", color="blue", weight=9];
6413 -> 1755[label="",style="solid", color="blue", weight=3];
3884[label="ceilingN0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (properFraction (Float (Neg (Succ yu242)) (Pos (Succ yu243))))\n  Integral a",fontsize=16,color="black",shape="box"];3884 -> 3906[label="",style="solid", color="black", weight=3];
1952[label="fromInt (Neg Zero `quot` Pos (Succ yu87))\n  Integral a",fontsize=16,color="blue",shape="box"];6414[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];1952 -> 6414[label="",style="solid", color="blue", weight=9];
6414 -> 1958[label="",style="solid", color="blue", weight=3];
6415[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1952 -> 6415[label="",style="solid", color="blue", weight=9];
6415 -> 1959[label="",style="solid", color="blue", weight=3];
6165 -> 6125[label="",style="dashed", color="red", weight=0];
6165[label="ceilingN (Float (Neg (Succ yu476)) (Neg (Succ yu477)))",fontsize=16,color="magenta"];6138[label="yu498 + fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="triangle"];6138 -> 6154[label="",style="solid", color="black", weight=3];
6166 -> 6125[label="",style="dashed", color="red", weight=0];
6166[label="ceilingN (Float (Neg (Succ yu476)) (Neg (Succ yu477)))",fontsize=16,color="magenta"];6140[label="yu499 + fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="triangle"];6140 -> 6155[label="",style="solid", color="black", weight=3];
6153[label="ceilingN0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (floatProperFractionFloat (Float (Neg (Succ yu476)) (Neg (Succ yu477))))\n  Integral a",fontsize=16,color="black",shape="box"];6153 -> 6163[label="",style="solid", color="black", weight=3];
2179[label="fromInt (Neg Zero `quot` Neg (Succ yu94))\n  Integral a",fontsize=16,color="blue",shape="box"];6418[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];2179 -> 6418[label="",style="solid", color="blue", weight=9];
6418 -> 2200[label="",style="solid", color="blue", weight=3];
6419[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];2179 -> 6419[label="",style="solid", color="blue", weight=9];
6419 -> 2201[label="",style="solid", color="blue", weight=3];
4375[label="ceilingCeiling0 (Float (Pos (Succ yu403)) (Pos (Succ yu404))) (LT == GT)\n  Integral a",fontsize=16,color="black",shape="triangle"];4375 -> 4630[label="",style="solid", color="black", weight=3];
5143 -> 4630[label="",style="dashed", color="red", weight=0];
5143[label="ceilingCeiling0 (Float (Pos (Succ yu417)) (Pos (Succ yu418))) False\n  Integral a",fontsize=16,color="magenta"];5143 -> 5201[label="",style="dashed", color="magenta", weight=3];
5143 -> 5202[label="",style="dashed", color="magenta", weight=3];
5141[label="yu417",fontsize=16,color="green",shape="box"];5142[label="yu418",fontsize=16,color="green",shape="box"];4157[label="ceilingN (Float (Pos (Succ Zero)) (Pos (Succ yu206)))\n  Integral a",fontsize=16,color="black",shape="box"];4157 -> 4173[label="",style="solid", color="black", weight=3];
1687[label="fromInt (Pos Zero `quot` Pos (Succ yu71))",fontsize=16,color="black",shape="box"];1687 -> 1706[label="",style="solid", color="black", weight=3];
1688[label="fromInt (Pos Zero `quot` Pos (Succ yu71))",fontsize=16,color="black",shape="box"];1688 -> 1707[label="",style="solid", color="black", weight=3];
6162[label="ceilingN0 (Float (Pos (Succ yu470)) (Neg (Succ yu471))) (fromInt (Pos (Succ yu470) `quot` Neg (Succ yu471)),Float (Pos (Succ yu470)) (Neg (Succ yu471)) - fromInt (Pos (Succ yu470) `quot` Neg (Succ yu471)))\n  Integral a",fontsize=16,color="black",shape="box"];6162 -> 6168[label="",style="solid", color="black", weight=3];
2198[label="Pos (primPlusNat yu2200 (Succ Zero))",fontsize=16,color="green",shape="box"];2198 -> 2210[label="",style="dashed", color="green", weight=3];
2199 -> 4381[label="",style="dashed", color="red", weight=0];
2199[label="primMinusNat (Succ Zero) yu2200",fontsize=16,color="magenta"];2199 -> 4396[label="",style="dashed", color="magenta", weight=3];
2199 -> 4397[label="",style="dashed", color="magenta", weight=3];
1754[label="fromInt (Pos Zero `quot` Neg (Succ yu78))",fontsize=16,color="black",shape="box"];1754 -> 1771[label="",style="solid", color="black", weight=3];
1755[label="fromInt (Pos Zero `quot` Neg (Succ yu78))",fontsize=16,color="black",shape="box"];1755 -> 1772[label="",style="solid", color="black", weight=3];
3906[label="ceilingN0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (floatProperFractionFloat (Float (Neg (Succ yu242)) (Pos (Succ yu243))))\n  Integral a",fontsize=16,color="black",shape="box"];3906 -> 3962[label="",style="solid", color="black", weight=3];
1958[label="fromInt (Neg Zero `quot` Pos (Succ yu87))",fontsize=16,color="black",shape="box"];1958 -> 1974[label="",style="solid", color="black", weight=3];
1959[label="fromInt (Neg Zero `quot` Pos (Succ yu87))",fontsize=16,color="black",shape="box"];1959 -> 1975[label="",style="solid", color="black", weight=3];
6154[label="error []",fontsize=16,color="red",shape="box"];6155 -> 2152[label="",style="dashed", color="red", weight=0];
6155[label="primPlusInt yu499 (fromInt (Pos (Succ Zero)))",fontsize=16,color="magenta"];6155 -> 6164[label="",style="dashed", color="magenta", weight=3];
6163[label="ceilingN0 (Float (Neg (Succ yu476)) (Neg (Succ yu477))) (fromInt (Neg (Succ yu476) `quot` Neg (Succ yu477)),Float (Neg (Succ yu476)) (Neg (Succ yu477)) - fromInt (Neg (Succ yu476) `quot` Neg (Succ yu477)))\n  Integral a",fontsize=16,color="black",shape="box"];6163 -> 6169[label="",style="solid", color="black", weight=3];
2200[label="fromInt (Neg Zero `quot` Neg (Succ yu94))",fontsize=16,color="black",shape="box"];2200 -> 2213[label="",style="solid", color="black", weight=3];
2201[label="fromInt (Neg Zero `quot` Neg (Succ yu94))",fontsize=16,color="black",shape="box"];2201 -> 2214[label="",style="solid", color="black", weight=3];
4630[label="ceilingCeiling0 (Float (Pos (Succ yu403)) (Pos (Succ yu404))) False\n  Integral a",fontsize=16,color="black",shape="triangle"];4630 -> 4654[label="",style="solid", color="black", weight=3];
5201[label="yu417",fontsize=16,color="green",shape="box"];5202[label="yu418",fontsize=16,color="green",shape="box"];4173[label="ceilingN0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (ceilingVu8 (Float (Pos (Succ Zero)) (Pos (Succ yu206))))\n  Integral a",fontsize=16,color="black",shape="box"];4173 -> 4185[label="",style="solid", color="black", weight=3];
1706[label="Integer (Pos Zero `quot` Pos (Succ yu71))",fontsize=16,color="green",shape="box"];1706 -> 1724[label="",style="dashed", color="green", weight=3];
1707[label="Pos Zero `quot` Pos (Succ yu71)",fontsize=16,color="black",shape="triangle"];1707 -> 1725[label="",style="solid", color="black", weight=3];
6168[label="fromInt (Pos (Succ yu470) `quot` Neg (Succ yu471))\n  Integral a",fontsize=16,color="blue",shape="box"];6423[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];6168 -> 6423[label="",style="solid", color="blue", weight=9];
6423 -> 6170[label="",style="solid", color="blue", weight=3];
6424[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];6168 -> 6424[label="",style="solid", color="blue", weight=9];
6424 -> 6171[label="",style="solid", color="blue", weight=3];
2210 -> 1668[label="",style="dashed", color="red", weight=0];
2210[label="primPlusNat yu2200 (Succ Zero)",fontsize=16,color="magenta"];2210 -> 2239[label="",style="dashed", color="magenta", weight=3];
4396[label="Succ Zero",fontsize=16,color="green",shape="box"];4397[label="yu2200",fontsize=16,color="green",shape="box"];1771[label="Integer (Pos Zero `quot` Neg (Succ yu78))",fontsize=16,color="green",shape="box"];1771 -> 1789[label="",style="dashed", color="green", weight=3];
1772[label="Pos Zero `quot` Neg (Succ yu78)",fontsize=16,color="black",shape="triangle"];1772 -> 1790[label="",style="solid", color="black", weight=3];
3962[label="ceilingN0 (Float (Neg (Succ yu242)) (Pos (Succ yu243))) (fromInt (Neg (Succ yu242) `quot` Pos (Succ yu243)),Float (Neg (Succ yu242)) (Pos (Succ yu243)) - fromInt (Neg (Succ yu242) `quot` Pos (Succ yu243)))\n  Integral a",fontsize=16,color="black",shape="box"];3962 -> 3994[label="",style="solid", color="black", weight=3];
1974[label="Integer (Neg Zero `quot` Pos (Succ yu87))",fontsize=16,color="green",shape="box"];1974 -> 2055[label="",style="dashed", color="green", weight=3];
1975[label="Neg Zero `quot` Pos (Succ yu87)",fontsize=16,color="black",shape="triangle"];1975 -> 2056[label="",style="solid", color="black", weight=3];
6164[label="yu499",fontsize=16,color="green",shape="box"];6169[label="fromInt (Neg (Succ yu476) `quot` Neg (Succ yu477))\n  Integral a",fontsize=16,color="blue",shape="box"];6426[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];6169 -> 6426[label="",style="solid", color="blue", weight=9];
6426 -> 6172[label="",style="solid", color="blue", weight=3];
6427[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];6169 -> 6427[label="",style="solid", color="blue", weight=9];
6427 -> 6173[label="",style="solid", color="blue", weight=3];
2213[label="Integer (Neg Zero `quot` Neg (Succ yu94))",fontsize=16,color="green",shape="box"];2213 -> 2242[label="",style="dashed", color="green", weight=3];
2214[label="Neg Zero `quot` Neg (Succ yu94)",fontsize=16,color="black",shape="triangle"];2214 -> 2243[label="",style="solid", color="black", weight=3];
4654[label="ceilingN (Float (Pos (Succ yu403)) (Pos (Succ yu404)))\n  Integral a",fontsize=16,color="black",shape="triangle"];4654 -> 4677[label="",style="solid", color="black", weight=3];
4185[label="ceilingN0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (properFraction (Float (Pos (Succ Zero)) (Pos (Succ yu206))))\n  Integral a",fontsize=16,color="black",shape="box"];4185 -> 4210[label="",style="solid", color="black", weight=3];
1724 -> 1707[label="",style="dashed", color="red", weight=0];
1724[label="Pos Zero `quot` Pos (Succ yu71)",fontsize=16,color="magenta"];1725[label="primQuotInt (Pos Zero) (Pos (Succ yu71))",fontsize=16,color="black",shape="box"];1725 -> 2184[label="",style="solid", color="black", weight=3];
6170[label="fromInt (Pos (Succ yu470) `quot` Neg (Succ yu471))",fontsize=16,color="black",shape="box"];6170 -> 6174[label="",style="solid", color="black", weight=3];
6171[label="fromInt (Pos (Succ yu470) `quot` Neg (Succ yu471))",fontsize=16,color="black",shape="box"];6171 -> 6175[label="",style="solid", color="black", weight=3];
2239[label="yu2200",fontsize=16,color="green",shape="box"];1789 -> 1772[label="",style="dashed", color="red", weight=0];
1789[label="Pos Zero `quot` Neg (Succ yu78)",fontsize=16,color="magenta"];1790[label="primQuotInt (Pos Zero) (Neg (Succ yu78))",fontsize=16,color="black",shape="box"];1790 -> 2315[label="",style="solid", color="black", weight=3];
3994[label="fromInt (Neg (Succ yu242) `quot` Pos (Succ yu243))\n  Integral a",fontsize=16,color="blue",shape="box"];6430[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];3994 -> 6430[label="",style="solid", color="blue", weight=9];
6430 -> 4110[label="",style="solid", color="blue", weight=3];
6431[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];3994 -> 6431[label="",style="solid", color="blue", weight=9];
6431 -> 4111[label="",style="solid", color="blue", weight=3];
2055 -> 1975[label="",style="dashed", color="red", weight=0];
2055[label="Neg Zero `quot` Pos (Succ yu87)",fontsize=16,color="magenta"];2056[label="primQuotInt (Neg Zero) (Pos (Succ yu87))",fontsize=16,color="black",shape="box"];2056 -> 2408[label="",style="solid", color="black", weight=3];
6172[label="fromInt (Neg (Succ yu476) `quot` Neg (Succ yu477))",fontsize=16,color="black",shape="box"];6172 -> 6176[label="",style="solid", color="black", weight=3];
6173[label="fromInt (Neg (Succ yu476) `quot` Neg (Succ yu477))",fontsize=16,color="black",shape="box"];6173 -> 6177[label="",style="solid", color="black", weight=3];
2242 -> 2214[label="",style="dashed", color="red", weight=0];
2242[label="Neg Zero `quot` Neg (Succ yu94)",fontsize=16,color="magenta"];2243[label="primQuotInt (Neg Zero) (Neg (Succ yu94))",fontsize=16,color="black",shape="box"];2243 -> 2469[label="",style="solid", color="black", weight=3];
4677[label="ceilingN0 (Float (Pos (Succ yu403)) (Pos (Succ yu404))) (ceilingVu8 (Float (Pos (Succ yu403)) (Pos (Succ yu404))))\n  Integral a",fontsize=16,color="black",shape="triangle"];4677 -> 4710[label="",style="solid", color="black", weight=3];
4210[label="ceilingN0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (floatProperFractionFloat (Float (Pos (Succ Zero)) (Pos (Succ yu206))))\n  Integral a",fontsize=16,color="black",shape="box"];4210 -> 4255[label="",style="solid", color="black", weight=3];
2184[label="Pos (primDivNatS Zero (Succ yu71))",fontsize=16,color="green",shape="box"];2184 -> 2540[label="",style="dashed", color="green", weight=3];
6174[label="Integer (Pos (Succ yu470) `quot` Neg (Succ yu471))",fontsize=16,color="green",shape="box"];6174 -> 6178[label="",style="dashed", color="green", weight=3];
6175[label="Pos (Succ yu470) `quot` Neg (Succ yu471)",fontsize=16,color="black",shape="triangle"];6175 -> 6179[label="",style="solid", color="black", weight=3];
2315[label="Neg (primDivNatS Zero (Succ yu78))",fontsize=16,color="green",shape="box"];2315 -> 2591[label="",style="dashed", color="green", weight=3];
4110[label="fromInt (Neg (Succ yu242) `quot` Pos (Succ yu243))",fontsize=16,color="black",shape="box"];4110 -> 4162[label="",style="solid", color="black", weight=3];
4111[label="fromInt (Neg (Succ yu242) `quot` Pos (Succ yu243))",fontsize=16,color="black",shape="box"];4111 -> 4163[label="",style="solid", color="black", weight=3];
2408[label="Neg (primDivNatS Zero (Succ yu87))",fontsize=16,color="green",shape="box"];2408 -> 2654[label="",style="dashed", color="green", weight=3];
6176[label="Integer (Neg (Succ yu476) `quot` Neg (Succ yu477))",fontsize=16,color="green",shape="box"];6176 -> 6180[label="",style="dashed", color="green", weight=3];
6177[label="Neg (Succ yu476) `quot` Neg (Succ yu477)",fontsize=16,color="black",shape="triangle"];6177 -> 6181[label="",style="solid", color="black", weight=3];
2469[label="Pos (primDivNatS Zero (Succ yu94))",fontsize=16,color="green",shape="box"];2469 -> 2708[label="",style="dashed", color="green", weight=3];
4710[label="ceilingN0 (Float (Pos (Succ yu403)) (Pos (Succ yu404))) (properFraction (Float (Pos (Succ yu403)) (Pos (Succ yu404))))\n  Integral a",fontsize=16,color="black",shape="triangle"];4710 -> 4741[label="",style="solid", color="black", weight=3];
4255[label="ceilingN0 (Float (Pos (Succ Zero)) (Pos (Succ yu206))) (fromInt (Pos (Succ Zero) `quot` Pos (Succ yu206)),Float (Pos (Succ Zero)) (Pos (Succ yu206)) - fromInt (Pos (Succ Zero) `quot` Pos (Succ yu206)))\n  Integral a",fontsize=16,color="black",shape="box"];4255 -> 4283[label="",style="solid", color="black", weight=3];
6178 -> 6175[label="",style="dashed", color="red", weight=0];
6178[label="Pos (Succ yu470) `quot` Neg (Succ yu471)",fontsize=16,color="magenta"];6179[label="primQuotInt (Pos (Succ yu470)) (Neg (Succ yu471))",fontsize=16,color="black",shape="box"];6179 -> 6182[label="",style="solid", color="black", weight=3];
2591 -> 2540[label="",style="dashed", color="red", weight=0];
2591[label="primDivNatS Zero (Succ yu78)",fontsize=16,color="magenta"];2591 -> 2935[label="",style="dashed", color="magenta", weight=3];
4162[label="Integer (Neg (Succ yu242) `quot` Pos (Succ yu243))",fontsize=16,color="green",shape="box"];4162 -> 4215[label="",style="dashed", color="green", weight=3];
4163[label="Neg (Succ yu242) `quot` Pos (Succ yu243)",fontsize=16,color="black",shape="triangle"];4163 -> 4216[label="",style="solid", color="black", weight=3];
2654 -> 2540[label="",style="dashed", color="red", weight=0];
2654[label="primDivNatS Zero (Succ yu87)",fontsize=16,color="magenta"];2654 -> 3468[label="",style="dashed", color="magenta", weight=3];
6180 -> 6177[label="",style="dashed", color="red", weight=0];
6180[label="Neg (Succ yu476) `quot` Neg (Succ yu477)",fontsize=16,color="magenta"];6181[label="primQuotInt (Neg (Succ yu476)) (Neg (Succ yu477))",fontsize=16,color="black",shape="box"];6181 -> 6183[label="",style="solid", color="black", weight=3];
2708 -> 2540[label="",style="dashed", color="red", weight=0];
2708[label="primDivNatS Zero (Succ yu94)",fontsize=16,color="magenta"];2708 -> 3569[label="",style="dashed", color="magenta", weight=3];
4741[label="ceilingN0 (Float (Pos (Succ yu403)) (Pos (Succ yu404))) (floatProperFractionFloat (Float (Pos (Succ yu403)) (Pos (Succ yu404))))\n  Integral a",fontsize=16,color="black",shape="box"];4741 -> 4773[label="",style="solid", color="black", weight=3];
4283[label="fromInt (Pos (Succ Zero) `quot` Pos (Succ yu206))\n  Integral a",fontsize=16,color="blue",shape="box"];6439[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];4283 -> 6439[label="",style="solid", color="blue", weight=9];
6439 -> 4319[label="",style="solid", color="blue", weight=3];
6440[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];4283 -> 6440[label="",style="solid", color="blue", weight=9];
6440 -> 4320[label="",style="solid", color="blue", weight=3];
6182[label="Neg (primDivNatS (Succ yu470) (Succ yu471))",fontsize=16,color="green",shape="box"];6182 -> 6184[label="",style="dashed", color="green", weight=3];
2935[label="yu78",fontsize=16,color="green",shape="box"];4215 -> 4163[label="",style="dashed", color="red", weight=0];
4215[label="Neg (Succ yu242) `quot` Pos (Succ yu243)",fontsize=16,color="magenta"];4216[label="primQuotInt (Neg (Succ yu242)) (Pos (Succ yu243))",fontsize=16,color="black",shape="box"];4216 -> 4259[label="",style="solid", color="black", weight=3];
3468[label="yu87",fontsize=16,color="green",shape="box"];6183[label="Pos (primDivNatS (Succ yu476) (Succ yu477))",fontsize=16,color="green",shape="box"];6183 -> 6185[label="",style="dashed", color="green", weight=3];
3569[label="yu94",fontsize=16,color="green",shape="box"];4773[label="ceilingN0 (Float (Pos (Succ yu403)) (Pos (Succ yu404))) (fromInt (Pos (Succ yu403) `quot` Pos (Succ yu404)),Float (Pos (Succ yu403)) (Pos (Succ yu404)) - fromInt (Pos (Succ yu403) `quot` Pos (Succ yu404)))\n  Integral a",fontsize=16,color="black",shape="box"];4773 -> 4931[label="",style="solid", color="black", weight=3];
4319[label="fromInt (Pos (Succ Zero) `quot` Pos (Succ yu206))",fontsize=16,color="black",shape="box"];4319 -> 4932[label="",style="solid", color="black", weight=3];
4320[label="fromInt (Pos (Succ Zero) `quot` Pos (Succ yu206))",fontsize=16,color="black",shape="box"];4320 -> 4933[label="",style="solid", color="black", weight=3];
6184 -> 5676[label="",style="dashed", color="red", weight=0];
6184[label="primDivNatS (Succ yu470) (Succ yu471)",fontsize=16,color="magenta"];6184 -> 6186[label="",style="dashed", color="magenta", weight=3];
6184 -> 6187[label="",style="dashed", color="magenta", weight=3];
4259[label="Neg (primDivNatS (Succ yu242) (Succ yu243))",fontsize=16,color="green",shape="box"];4259 -> 5166[label="",style="dashed", color="green", weight=3];
6185 -> 5676[label="",style="dashed", color="red", weight=0];
6185[label="primDivNatS (Succ yu476) (Succ yu477)",fontsize=16,color="magenta"];6185 -> 6188[label="",style="dashed", color="magenta", weight=3];
6185 -> 6189[label="",style="dashed", color="magenta", weight=3];
4931[label="fromInt (Pos (Succ yu403) `quot` Pos (Succ yu404))\n  Integral a",fontsize=16,color="blue",shape="box"];6444[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];4931 -> 6444[label="",style="solid", color="blue", weight=9];
6444 -> 5633[label="",style="solid", color="blue", weight=3];
6445[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];4931 -> 6445[label="",style="solid", color="blue", weight=9];
6445 -> 5634[label="",style="solid", color="blue", weight=3];
4932[label="Integer (Pos (Succ Zero) `quot` Pos (Succ yu206))",fontsize=16,color="green",shape="box"];4932 -> 5635[label="",style="dashed", color="green", weight=3];
4933[label="Pos (Succ Zero) `quot` Pos (Succ yu206)",fontsize=16,color="black",shape="triangle"];4933 -> 5636[label="",style="solid", color="black", weight=3];
6186[label="yu470",fontsize=16,color="green",shape="box"];6187[label="yu471",fontsize=16,color="green",shape="box"];5166 -> 5676[label="",style="dashed", color="red", weight=0];
5166[label="primDivNatS (Succ yu242) (Succ yu243)",fontsize=16,color="magenta"];5166 -> 5687[label="",style="dashed", color="magenta", weight=3];
5166 -> 5688[label="",style="dashed", color="magenta", weight=3];
6188[label="yu476",fontsize=16,color="green",shape="box"];6189[label="yu477",fontsize=16,color="green",shape="box"];5633[label="fromInt (Pos (Succ yu403) `quot` Pos (Succ yu404))",fontsize=16,color="black",shape="box"];5633 -> 5810[label="",style="solid", color="black", weight=3];
5634[label="fromInt (Pos (Succ yu403) `quot` Pos (Succ yu404))",fontsize=16,color="black",shape="box"];5634 -> 5811[label="",style="solid", color="black", weight=3];
5635 -> 4933[label="",style="dashed", color="red", weight=0];
5635[label="Pos (Succ Zero) `quot` Pos (Succ yu206)",fontsize=16,color="magenta"];5636[label="primQuotInt (Pos (Succ Zero)) (Pos (Succ yu206))",fontsize=16,color="black",shape="box"];5636 -> 5816[label="",style="solid", color="black", weight=3];
5687[label="yu242",fontsize=16,color="green",shape="box"];5688[label="yu243",fontsize=16,color="green",shape="box"];5810[label="Integer (Pos (Succ yu403) `quot` Pos (Succ yu404))",fontsize=16,color="green",shape="box"];5810 -> 5925[label="",style="dashed", color="green", weight=3];
5811[label="Pos (Succ yu403) `quot` Pos (Succ yu404)",fontsize=16,color="black",shape="triangle"];5811 -> 5926[label="",style="solid", color="black", weight=3];
5816[label="Pos (primDivNatS (Succ Zero) (Succ yu206))",fontsize=16,color="green",shape="box"];5816 -> 5931[label="",style="dashed", color="green", weight=3];
5925 -> 5811[label="",style="dashed", color="red", weight=0];
5925[label="Pos (Succ yu403) `quot` Pos (Succ yu404)",fontsize=16,color="magenta"];5926[label="primQuotInt (Pos (Succ yu403)) (Pos (Succ yu404))",fontsize=16,color="black",shape="box"];5926 -> 5945[label="",style="solid", color="black", weight=3];
5931 -> 5676[label="",style="dashed", color="red", weight=0];
5931[label="primDivNatS (Succ Zero) (Succ yu206)",fontsize=16,color="magenta"];5931 -> 5952[label="",style="dashed", color="magenta", weight=3];
5931 -> 5953[label="",style="dashed", color="magenta", weight=3];
5945[label="Pos (primDivNatS (Succ yu403) (Succ yu404))",fontsize=16,color="green",shape="box"];5945 -> 5962[label="",style="dashed", color="green", weight=3];
5952[label="Zero",fontsize=16,color="green",shape="box"];5953[label="yu206",fontsize=16,color="green",shape="box"];5962 -> 5676[label="",style="dashed", color="red", weight=0];
5962[label="primDivNatS (Succ yu403) (Succ yu404)",fontsize=16,color="magenta"];5962 -> 5973[label="",style="dashed", color="magenta", weight=3];
5962 -> 5974[label="",style="dashed", color="magenta", weight=3];
5973[label="yu403",fontsize=16,color="green",shape="box"];5974[label="yu404",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                          ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yu300000000), Succ(yu4340000)) → new_primPlusNat(yu300000000, yu4340000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(yu300000000), Succ(yu4340000)) → new_primPlusNat(yu300000000, yu4340000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

                          ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(yu4060), Succ(yu3900)) → new_primMinusNat(yu4060, yu3900)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat(Succ(yu4060), Succ(yu3900)) → new_primMinusNat(yu4060, yu3900)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                          ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yu1130)) → new_primMulNat(yu1130)

From the DPs we obtained the following set of size-change graphs:

new_primMulNat(Succ(yu1130)) → new_primMulNat(yu1130)
The graph contains the following edges 1 > 1

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                          ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(yu424, yu425) → new_primDivNatS(yu424, yu425)
new_primDivNatS1(Succ(yu4880), Succ(yu4890), yu490) → new_primDivNatS1(yu4880, yu4890, yu490)
new_primDivNatS00(yu30000, yu31000) → new_primDivNatS00(yu30000, yu31000)
new_primDivNatS03(yu494, yu495, Succ(yu4960), Zero) → new_primDivNatS01(yu494, Succ(yu495))
new_primDivNatS0(Succ(yu30000), Succ(yu31000)) → new_primDivNatS00(yu30000, yu31000)
new_primDivNatS0(Succ(yu30000), Zero) → new_primDivNatS01(yu30000, Zero)
new_primDivNatS0(Zero, Zero) → new_primDivNatS02
new_primDivNatS03(yu494, yu495, Succ(yu4960), Succ(yu4970)) → new_primDivNatS03(yu494, yu495, yu4960, yu4970)
new_primDivNatS03(yu494, yu495, Zero, Zero) → new_primDivNatS01(yu494, Succ(yu495))
new_primDivNatS01(yu424, yu425) → new_primDivNatS(yu424, yu425)
new_primDivNatS02 → new_primDivNatS1(Zero, Zero, Zero)
new_primDivNatS1(Succ(yu4880), Zero, yu490) → new_primDivNatS2(yu4880, yu490)
new_primDivNatS2(yu451, yu452) → new_primDivNatS0(yu451, yu452)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs with 9 less nodes.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ NonTerminationProof

                                    ↳ QDP

                                    ↳ QDP

                                    ↳ QDP

                          ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS00(yu30000, yu31000) → new_primDivNatS00(yu30000, yu31000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_primDivNatS00(yu30000, yu31000) → new_primDivNatS00(yu30000, yu31000)

The TRS R consists of the following rules:none

s = new_primDivNatS00(yu30000, yu31000) evaluates to t =new_primDivNatS00(yu30000, yu31000)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_primDivNatS00(yu30000, yu31000) to new_primDivNatS00(yu30000, yu31000).

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ NonTerminationProof

                                    ↳ QDP

                                    ↳ QDP

                          ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(yu424, yu425) → new_primDivNatS(yu424, yu425)

The TRS R consists of the following rules:none

s = new_primDivNatS(yu424, yu425) evaluates to t =new_primDivNatS(yu424, yu425)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_primDivNatS(yu424, yu425) to new_primDivNatS(yu424, yu425).

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ QDPSizeChangeProof

                                    ↳ QDP

                          ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS1(Succ(yu4880), Succ(yu4890), yu490) → new_primDivNatS1(yu4880, yu4890, yu490)

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS1(Succ(yu4880), Succ(yu4890), yu490) → new_primDivNatS1(yu4880, yu4890, yu490)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ QDPSizeChangeProof

                          ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS03(yu494, yu495, Succ(yu4960), Succ(yu4970)) → new_primDivNatS03(yu494, yu495, yu4960, yu4970)

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS03(yu494, yu495, Succ(yu4960), Succ(yu4970)) → new_primDivNatS03(yu494, yu495, yu4960, yu4970)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

Haskell To QDPs

primDivNatS0	x y True	= Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0	x y False	= Zero

primModNatS0	x y True	= primModNatS (primMinusNatS x y) (Succ y)
primModNatS0	x y False	= Succ x

ceilingCeiling0	xx True	= ceilingN xx + 1
ceilingCeiling0	xx False	= ceilingN xx